Haskell is not a theorem prover, and I doubt it can be made one. You can encode some properties of data via the type system, but it's still a general purpose la

Haskell is not a theorem prover, and I doubt it can be made one. You can encode some properties of data via the type system, but it's still a general purpose language. Agda on the other hand is a theorem prover, but much less general purpose.