Jean Abou Samra (new account) on Nostr: nprofile1q…4rrqe I'm glad you're implementing your proof assistant with this in ...

nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyzf5l64n2xk9azdrt6c96nwshexx45v4sduj7cyakmw005afuu05jm4rrqe (nprofile…rrqe) I'm glad you're implementing your proof assistant with this in mind. Lean is excellent in many respects but (although everybody talks about this as an advantage over other proof assistants) I never got used to its editing experience. I find it super distracting to have the infoview updating constantly with new errors and warnings as I type. Not to mention the frustration when I stare at the goal thinking, start writing a tactic, and the error on the incomplete line makes the goal disappear.