3 ms·
You are using the word Axiom in a non-standard way. Can you give an example of how you would state an Axiom in Haskell? Here is an example of how it is done in
by deterministic 3y ago
You are using the word Axiom in a non-standard way.
Can you give an example of how you would state an Axiom in Haskell? Here is an example of how it is done in LEAN:
axiom propext {a b : Prop} : (a <-> b) → a = b
It declares Propositional Extensionality to be true with no evidence/proof.