4 ms·

Have you looked into Idris2 at all. While looking into these theorum provers, it always felt like they had an impedance mismatch with normal programming. Idris

by aeonik 3y ago

Have you looked into Idris2 at all. While looking into these theorum provers, it always felt like they had an impedance mismatch with normal programming. Idris2 portends to a general purpose language that also has a more advanced type system for the theorum proving. https://github.com/idris-lang/Idris2 https://github.com/idris-lang/Idris2

atomicnature 3y ago
That's interesting; no I wasn't aware of it. Will check it out sometime, thanks.
- iso8859-1 3y ago
  There's a list of packages here: https://github.com/stefan-hoeck/idris2-pack-db/blob/main/STATUS.md https://github.com/stefan-hoeck/idris2-pack-db/blob/main/STA...