Library Coq.Program.Utils
Various syntaxic shortands 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 ident,
y ident,
at level 10) :
type_scope.
Generates an obligation to prove False.
Notation " ! " := (
False_rect _ _) :
program_scope.
Delimit Scope program_scope with prg.
Abbreviation for first projection and hiding of proofs of subset objects.
Notation " ` t " := (
proj1_sig t) (
at level 10,
t at next level) :
program_scope.
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