Got lost down a weird rabbit hole (as usual) and as a result ended up porting Software Foundations' total and partial maps to Lean 4:
Conversation
Somethings I like about Lean 4:
As was the case in previous versions, I really like how you can get a namespace for every definition in Lean, instead of having to resort to ad-hoc prefixes that you have to use in other theorem provers.
1
I also love how Lean 4's tactics are hygenic by default. If you want to explicitly mention a name in a proof, you need to bind it first in the tactic's invocation, or Lean will get grumpy with you.
Replying to
The labelled arguments in Lean 4 are also super great - they make reading code much nicer, and you can arguments out of order.
1
2
Also the `.` operator seems to work reasonably well! IIUC it seems to use something like what Barret, , and were using in Klister (github.com/gelisam/klister) - ie. where elaboration is deferred until the type is known.
2