|
|
|
|
|
|
by iamrecursion
3127 days ago
|
|
|
I should add that something like FStar [0] combines the capabilities of automated theorem proving and a more manual-proof-based dependent type system like that in Idris. It doesn’t have some of the power of Idris’ elaborator reflection, for example, but it can eliminate many long-winded manual proofs via the SMT solver. [0] https://www.fstar-lang.org/ |
|
|