I am trying to extract a witness from a coq sentence (or something like that).
I have something similar to
Parameter atom_fresh_for_list : forall (xs : list atom), {x : atom | ~ List.In x xs}.
(as proved later, with an explicit type for atom :
Lemma atom_fresh_for_list : forall (xs : list nat), { n : nat | ~ List.In n xs }.
How to extract such x ? Documentation says
From this (there is xp) we can, in turn, extract our witness x: A (using an exception construct such as a match)
but I don’t understand how it works ....
It also says
Given A: Type and P: A-> Prop, the construction {x: A | P x} is a type
But if I try something like Parameter C : {x : atom | x \notin xs} Parameter C : {x : atom | x \notin xs} , it gives
Error: The term "C" has type "{x : atom | x \notin xs}" which should be Set, Prop or Type.
source share