# 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 ident, y ident, at level 10) : type_scope.

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.

Notation " x '`=' y " := ((x :>) = (y :>)) (at level 70) : program_scope.

Require Import Coq.Bool.Sumbool.

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