|
|
|
|
|
|
by namarkiv
3484 days ago
|
|
|
I would like to emphasize that this gives you a theorem prover "inside" haskell, unlike coq/agda where you need to do program extraction. This means you can combine proofs and programs without a significant impact to the runtime performance. |
|
|