coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Daniel Schepler <dschepler AT gmail.com>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] problem with tactic-generated terms
- Date: Sat, 13 Sep 2014 06:01:21 -0700
On Fri, Sep 12, 2014 at 6:41 PM, Jonathan
<jonikelee AT gmail.com>
wrote:
> Well, either I have to hope reality is sufficiently paraconsistent, or
> investigate an alternative erasability mechanism. Maybe the one Daniel
> Shepler is suggesting is suitable.
Hmm, my first attempt at packaging the idea was:
Record Erasable (A:Type) := {
has_value : A -> Prop;
is_singleton : exists! x:A, has_value x
}.
But it seems that's not quite erasable: once I get everything set up,
on Coq 8.4pl4 it extracts to
type 'a erasable =
| Build_Erasable
type 'a vector =
| Vector_nil
| Vector_cons of 'a * nat erasable * 'a vector
I wonder if it would be possible to add a feature to trunk, so that if
every element of a record is erasable, the record itself is also
considered erasable.
The next thing I tried was:
Definition Erasable (A:Type) :=
{ has_value : A -> Prop | exists! x:A, has_value x }.
But that gets a much uglier extraction with __ all over the place.
--
Daniel Schepler
- Re: [Coq-Club] problem with tactic-generated terms, (continued)
- Re: [Coq-Club] problem with tactic-generated terms, Jonathan, 09/12/2014
- Re: [Coq-Club] problem with tactic-generated terms, Daniel Schepler, 09/12/2014
- Re: [Coq-Club] problem with tactic-generated terms, Greg Morrisett, 09/12/2014
- Re: [Coq-Club] problem with tactic-generated terms, Jonathan, 09/13/2014
- Re: [Coq-Club] problem with tactic-generated terms, Adam Chlipala, 09/13/2014
- Re: [Coq-Club] problem with tactic-generated terms, Jonathan, 09/13/2014
- Re: [Coq-Club] problem with tactic-generated terms, Matthieu Sozeau, 09/13/2014
- Re: [Coq-Club] problem with tactic-generated terms, Robert Dockins, 09/13/2014
- Re: [Coq-Club] problem with tactic-generated terms, Jonathan, 09/13/2014
- Re: [Coq-Club] problem with tactic-generated terms, Matthieu Sozeau, 09/13/2014
- Re: [Coq-Club] problem with tactic-generated terms, Daniel Schepler, 09/13/2014
- Re: [Coq-Club] problem with tactic-generated terms, Hugo Herbelin, 09/13/2014
- Re: [Coq-Club] problem with tactic-generated terms, Jonathan, 09/14/2014
- Re: [Coq-Club] problem with tactic-generated terms, Hugo Herbelin, 09/15/2014
- Re: [Coq-Club] problem with tactic-generated terms, Jonathan, 09/15/2014
- Re: [Coq-Club] problem with tactic-generated terms, Hugo Herbelin, 09/15/2014
- Re: [Coq-Club] problem with tactic-generated terms, Jonathan, 09/13/2014
- Re: [Coq-Club] problem with tactic-generated terms, Greg Morrisett, 09/12/2014
- Re: [Coq-Club] problem with tactic-generated terms, Daniel Schepler, 09/12/2014
- Re: [Coq-Club] problem with tactic-generated terms, Jonathan, 09/12/2014
- Re: [Coq-Club] problem with tactic-generated terms, Jonathan, 09/13/2014
- Re: [Coq-Club] problem with tactic-generated terms, Daniel Schepler, 09/13/2014
- Re: [Coq-Club] problem with tactic-generated terms, Daniel Schepler, 09/13/2014
Archive powered by MHonArc 2.6.18.