Closed mdokomath closed 3 months ago
Adds a tactic for easier work with constrictive_indefinite_description, which I needed reasonably often in a couple of my recent projects.
To me, the tactic has a distinct des_something feel about it.
See if the addition of it to Hahn makes sense.
Adds a tactic for easier work with constrictive_indefinite_description, which I needed reasonably often in a couple of my recent projects.
To me, the tactic has a distinct des_something feel about it.
See if the addition of it to Hahn makes sense.