Hi all! I'm looking for pointers to useful custom tactics and other proof automation (both general and domain-specific) in proof assistants other than Coq for my survey paper. Let me know if you know of anything noteworthy!
11
8
15
Conversation
Some of the things implemented using Idris' elaborator reflection could be interesting! github.com/jdevuyst/reken
1
3
I wonder if refinement types (backed by a constraint solver) could also come under the banner of proof automation.