Example of non-constructive proofs in ATS?

Google Group
1

I noticed that in the official introductionhttp://www.ats-lang.org/DOCUMENT/INT2PROGINATS/HTML/c2948.html it’s
said that “proofs encoded in ATS/LF are not required to be constructive”,
but so far all the proof examples in the introduction look to be
constructive to me. Can someone please show me a non-constructive proof in
ATS?

2

There are many non-constructive proofs encoded in ATS in the following file:

http://www.cs.bu.edu/~hwxi/academic/courses/CS511/Spring12/code/Logics/PropLogic.dats

For instance,

prfun ExcludedMiddle {A:prop} (): PDISJ (A, PNEG (A))

prfun PeirceLaw {P,Q:prop} (): PIMPL (PIMPL (PIMPL (P, Q), P), P)

prfun DoubleNegationByLEM {A:prop} (pf1: PNEG (PNEG (A)), pf2: PDISJ (A, PNEG (A))): AOn Sunday, December 8, 2013 12:50:09 AM UTC-5, Ming Lei wrote:

I noticed that in the official introductionhttp://www.ats-lang.org/DOCUMENT/INT2PROGINATS/HTML/c2948.html it’s
said that “proofs encoded in ATS/LF are not required to be constructive”,
but so far all the proof examples in the introduction look to be
constructive to me. Can someone please show me a non-constructive proof in
ATS?