Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] problem with tactic-generated terms

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] problem with tactic-generated terms


Chronological Thread 
  • 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



Archive powered by MHonArc 2.6.18.

Top of Page