Re: Derive ET from DN in calculus of constructions

Olaf Klinke <[email protected]>
Newsgroups gmane.comp.lang.haskell.cafe
Message-ID <[email protected]> 
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

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
lmpx.com only provides a reader for public news (NNTP) servers. It is not affiliated with the servers or forums shown here and is not responsible for the content of articles, which is written by their respective authors.