The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 21/06/2013 16:07, Enrico Tassi wrote:
> I did not look at the code, but I'm curious.  What happens if you do:
> 
>   assert True >> [ abstract( exact I ) | idtac ].
> 
> And in the even more trickier case, if you do:
> 
>   Goal (Type /\ Type) /\ True.
>   split; [ split >> [ exact Type | exact Type ] | exact Type ].
> 
> which is the resulting proof term?
>  (Conj (Conj Type_i Type_i) Type_i)  or  (Conj (Conj Type_i Type_j) Type_k)

In the first case, it will die in a horrible suffering, because of the
current implementation of abstract (and admit) whose defects you're
aware of.

I admit that I did not think about the second case, which is tricky
indeed. Nonetheless, it is quite easy to freshen the universes in the
generated term, and let the universe constraint solver deal with it.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature