The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

{ x : foo & bar } and { x : foo | bar } are different types (sigT and 
sig respectively)
exist produces sig, you need existT for sigT

(sig accepts only Prop for the second component, the difference is 
useful for extraction)

Gaëtan Gilbert

On 08/11/2018 20:50, Morgan Sinclaire wrote:
> I'm having an issue with a certain construction. The details/background 
> shouldn't be important, but I have types "formula", "ord", and "nf : ord 
> -> Prop" defined (the latter two taken from a paper). I'm trying to 
> build a new type "ptree" and assign members of type "e_0" to it in a 
> certain way. Here's the relevant (grossly abridged) part of my code:
>
> Definition e_0 : Set := {a : ord & nf a}.
>
> Theorem Zero_nf : nf Zero.
> Proof. apply zero_nf. Qed.
>
> Inductive ptree : Type :=
> | node_p : formula -> e_0 -> ptree.
>
> Fixpoint finite_valid_p (t : ptree) : Prop :=
>    match t with
>    | node_p f alpha => alpha = exist nf Zero Zero_nf
>    end.
>
> When I run that, the Fixpoint fails with the error:
>
> "The term "exist nf Zero Zero_nf" has type "{x : ord | nf x}"
> while it is expected to have type "e_0"."
>
> Which I don't understand, since that's /exactly/ how I defined e_0. On 
> the other hand, when I changed the definition of "ptree" to:
>
> Inductive ptree : Type :=
> | node_p : formula -> {x : ord | nf x} -> ptree.
>
> Then everything works. What am I doing wrong here?
>
> Thanks,
> Morgan