[aeonik]

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

[atomicnature]

That's interesting; no I wasn't aware of it. Will check it out sometime, thanks.

[iso8859-1]

There's a list of packages here: https://github.com/stefan-hoeck/idris2-pack-db/blob/main/STA...