5 ms·
Very interesting. I was thinking something similar could be done in Haskell.
by dyoder 12y ago
Very interesting. I was thinking something similar could be done in Haskell.
- quchen 12y agoHaskell 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.