Better syntax for pm_terms

Open markusdemedeiros opened this issue 2 months ago • 1 comments

Proofmode terms currently use Iris syntax, which specializes terms using a clunky with and $! for Iris and Lean level variables separately.

Is a cleaner syntax possible?

Dec 04 '25 22:12 markusdemedeiros

You could just borrow the cases/rcases syntax. It comes with nice code actions.

Dec 15 '25 14:12 Shreyas4991