The Coq mailing list

[Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>]

My point was : Empty_set -> Empty_set = unit is a crazy thing, doesn't
it ? 
So are universal subterms an issue in Type ?

But as Arnaud said, I need to wake up before thinking further :-)


Le vendredi 13 décembre 2013 à 04:20 -0500, Maxime Dénès a écrit :
> Hi Pierre,
> 
> I am not sure to see what you mean. The term (fun (x : Empty) => match x 
> with end) will still be considered by the current termination checker as 
> a subterm of any recursive argument, am I wrong? So the issue does not 
> seem specific to Prop.