coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Vladimir Voevodsky <vladimir AT ias.edu>
- To: Coq Club <coq-club AT inria.fr>
- Cc: "Prof. Vladimir Voevodsky" <vladimir AT ias.edu>, homotopytypetheory <homotopytypetheory AT googlegroups.com>
- Subject: [Coq-Club] eliminators
- Date: Thu, 23 Oct 2014 10:34:43 +0100
Hello,
is there a way to make Coq print proof terms using eliminators when these
proof terms are constructed using
eliminators?
For example “destruct” uses the eliminators but the proof terms constructed
with destruct are printed in terms of “match” even
when I request the corresponding eliminator to be opaque. An example code is
below.
This makes it very difficult for me to teach Coq to mathematicians. I can
explain eliminators to them but I do not know how to explain
match to them and I am not even sure that a semantically adequate theory of
dependent “match” exists. In any event even if it does
exist it is still not right that when I request something to be opaque Coq
unfolds it without asking.
***
Opaque Empty_set_rect.
Opaque Empty_set_rec.
Opaque Empty_set_ind.
Definition test { X : UU } : Empty_set -> X .
Proof . intros X H . destruct H . Defined.
Print test.
Definition test' { X : UU } : Empty_set -> X := fun H => Empty_set_rect ( fun
x => X ) H .
Print test' .
***
Vladimir.
- [Coq-Club] eliminators, Vladimir Voevodsky, 10/23/2014
- Re: [Coq-Club] eliminators, Beta Ziliani, 10/23/2014
- Re: [Coq-Club] eliminators, Vladimir Voevodsky, 10/23/2014
- Re: [Coq-Club] eliminators, Vladimir Voevodsky, 10/23/2014
- Re: [Coq-Club] eliminators, Beta Ziliani, 10/23/2014
- Re: [Coq-Club] eliminators, Beta Ziliani, 10/23/2014
Archive powered by MHonArc 2.6.18.