[Haskell-cafe] Derive ET from DN in calculus of constructions

Olaf Klinke olf at aatal-apotheke.de
Wed Nov 6 06:18:39 UTC 2024


The derivation of the double negation of ET is in line 243 of
https://hub.darcs.net/olf/haskell_for_mathematicians/browse/haskell_for_logicians.lhs
Then use DN on that term, as Tom Smeding suggested. 

Olaf



More information about the Haskell-Cafe mailing list