The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

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