I mentioned in another comment, but that worse user experience is also going to exist with Idris. It's not a theorem prover, you can just use it as one.
replyIdris has pi and sigma types, dependent pattern matching, view patterns, totality checking, proof search, interactive case splitting, etc, etc.
replyIt is orders of magnitude better then Haskell where the best you can do is hacky bullshit with singletons, GADTs, and type families.
Sure, but what I'm saying is that still doesn't make it nice to use as a proof assistant. As you say, the UX isn't there, no matter how much more terse the type system is at certain things in native semantics. Idris is designed to express executable programs, it has a wildly different grain to it than Lean or any other system designed to be used as a general proof assistant from the ground up.
replyI agree that Lean or any of the other languages I listed would be a better choice then Idris and despite how I wrote my original post I wouldn't recommend Idris to someone who explicitly wanted a theorem prover.
reply