The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Hi all,

I did find out that { H : a = B | ... } has type Prop
under 8.5pl2 ? Why is this so ? This implies that
such a result allows to prove something like

Theorem strange X (P : forall x y, x = y -> Prop) (x y : X) :
   (exists H : x = y, P x y H) -> { H : x = y | P _ _ H }.
Proof.
  intros (H & ?); exists H; auto.
Qed.

Does this not break extraction ?

Best regards,

Dominique

-----

Le 14/11/2016 à 13:35, Randy Pollack a écrit :
> Page 134 of the reference manual (8.5pl2) describes the reduction rule
> for a fixpoint application:
> 
> ================================
> The reduction for fixpoints is:
>    [...]
> when aki starts with a constructor. This last restriction is needed in
> order to keep strong normalization.
> ==================================
> 
> Is is known if this last restriction is needed when the context in
> which the fixpoint application is well typed doesn't contain any
> axioms?  (References or examples?)
> 
> What about for specific axioms, such as functional extensionality, axiom K, 
> ...?
> 
> Thanks,
> --Randy
>