Library Coq.Program.Utils
Various syntactic shorthands that are useful with Program.
A simpler notation for subsets defined on a cartesian product.
Notation "{ ( x , y ) : A | P }" :=
(sig (fun anonymous : A => let (x,y) := anonymous in P))
(x name, y name, at level 10) : type_scope.
Declare Scope program_scope.
Delimit Scope program_scope with prg.
Generates an obligation to prove False.
Abbreviation for first projection and hiding of proofs of subset objects.
Coerces objects to their support before comparing them.
Construct a dependent disjunction from a boolean.
The notations in_right and in_left construct objects of a dependent disjunction.
Hide proofs and generates obligations when put in a term.
Extraction directives