Usability issue
There is no refl tactic. Closing a reflexivity goal (e.g. (= Nat zero zero)) requires writing exact (same ...) explicitly. This is the single most common proof step in any dependently-typed proof assistant, and its absence creates unnecessary friction especially for new users.
Context
Encountered constantly when working through even basic Pie proofs in the interactive proof assistant. Any proof that ends with a reflexive equality requires dropping out of the tactic palette and writing an exact term, breaking the flow of tactic-based proof construction.
Suggested improvement
Add a refl tactic that automatically closes goals of the form (= A a a) by applying same. If the two sides are not definitionally equal, produce a clear error message explaining why reflexivity does not apply.
Usability issue
There is no
refltactic. Closing a reflexivity goal (e.g.(= Nat zero zero)) requires writingexact (same ...)explicitly. This is the single most common proof step in any dependently-typed proof assistant, and its absence creates unnecessary friction especially for new users.Context
Encountered constantly when working through even basic Pie proofs in the interactive proof assistant. Any proof that ends with a reflexive equality requires dropping out of the tactic palette and writing an exact term, breaking the flow of tactic-based proof construction.
Suggested improvement
Add a
refltactic that automatically closes goals of the form(= A a a)by applyingsame. If the two sides are not definitionally equal, produce a clear error message explaining why reflexivity does not apply.