From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 25 Jul 2008 15:12:53 +0200 Subject: Imported Upstream version 8.2~beta3+dfsg --- theories/Program/Utils.v | 56 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 56 insertions(+) create mode 100644 theories/Program/Utils.v (limited to 'theories/Program/Utils.v') diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v new file mode 100644 index 00000000..21eee0ca --- /dev/null +++ b/theories/Program/Utils.v @@ -0,0 +1,56 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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. *) + +Notation " x '`=' y " := ((x :>) = (y :>)) (at level 70) : program_scope. + +Require Import Coq.Bool.Sumbool. + +(** Construct a dependent disjunction from a boolean. *) + +Notation dec := sumbool_of_bool. + +(** The notations [in_right] and [in_left] construct objects of a dependent disjunction. *) + +(** Hide proofs and generates obligations when put in a term. *) + +Notation "'in_left'" := (@left _ _ _) : program_scope. +Notation "'in_right'" := (@right _ _ _) : program_scope. + +(** Extraction directives *) +(* +Extraction Inline proj1_sig. +Extract Inductive unit => "unit" [ "()" ]. +Extract Inductive bool => "bool" [ "true" "false" ]. +Extract Inductive sumbool => "bool" [ "true" "false" ]. +(* Extract Inductive prod "'a" "'b" => " 'a * 'b " [ "(,)" ]. *) +(* Extract Inductive sigT => "prod" [ "" ]. *) +*) \ No newline at end of file -- cgit v1.2.3