+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| A.Asperti, C.Sacerdoti Coen, *)
+(* ||A|| E.Tassi, S.Zacchiroli *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU Lesser General Public License Version 2.1 *)
+(* *)
+(**************************************************************************)
+
(* Logic system *)
inductive Imply (A,B:CProp) : CProp ≝
interpretation "Imply_intro_ko_2" 'Imply_intro_ko_2 ab \eta.b =
(cast _ _ (show ab (cast _ _ (Imply_intro _ _ b)))).
-notation < "\infrule hbox(\emsp b \emsp) ab (⇒\sub\i \emsp ident H) " with precedence 19
+notation < "maction (\infrule hbox(\emsp b \emsp) ab (⇒\sub\i \emsp ident H) ) (\vdots)" with precedence 19
for @{ 'Imply_intro_ok_1 $ab (λ${ident H}:$p.$b) }.
interpretation "Imply_intro_ok_1" 'Imply_intro_ok_1 ab \eta.b =
(show ab (Imply_intro _ _ b)).
interpretation "Imply_elim_ko_2" 'Imply_elim_ko_2 ab a b =
(cast _ _ (show b (cast _ _ (Imply_elim _ _ (cast _ _ ab) (cast _ _ a))))).
-notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (⇒\sub\e) " with precedence 19
+notation < "maction (\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (⇒\sub\e) ) (\vdots)" with precedence 19
for @{ 'Imply_elim_ok_1 $ab $a $b }.
interpretation "Imply_elim_ok_1" 'Imply_elim_ok_1 ab a b =
(show b (Imply_elim _ _ ab a)).
interpretation "And_intro_ko_2" 'And_intro_ko_2 a b ab =
(cast _ _ (show ab (cast _ _ (And_intro _ _ a b)))).
-notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) ab (∧\sub\i)" with precedence 19
+notation < "maction (\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) ab (∧\sub\i)) (\vdots)" with precedence 19
for @{ 'And_intro_ok_1 $a $b $ab }.
interpretation "And_intro_ok_1" 'And_intro_ok_1 a b ab =
(show ab (And_intro _ _ a b)).
interpretation "And_elim_l_ko_2" 'And_elim_l_ko_2 ab a =
(cast _ _ (show a (cast _ _ (And_elim_l _ _ (cast _ _ ab))))).
-notation < "\infrule hbox(\emsp ab \emsp) a (∧\sub(\e_\l))" with precedence 19
+notation < "maction (\infrule hbox(\emsp ab \emsp) a (∧\sub(\e_\l))) (\vdots)" with precedence 19
for @{ 'And_elim_l_ok_1 $ab $a }.
interpretation "And_elim_l_ok_1" 'And_elim_l_ok_1 ab a =
(show a (And_elim_l _ _ ab)).
interpretation "And_elim_r_ko_2" 'And_elim_r_ko_2 ab a =
(cast _ _ (show a (cast _ _ (And_elim_r _ _ (cast _ _ ab))))).
-notation < "\infrule hbox(\emsp ab \emsp) a (∧\sub(\e_\r))" with precedence 19
+notation < "maction (\infrule hbox(\emsp ab \emsp) a (∧\sub(\e_\r))) (\vdots)" with precedence 19
for @{ 'And_elim_r_ok_1 $ab $a }.
interpretation "And_elim_r_ok_1" 'And_elim_r_ok_1 ab a =
(show a (And_elim_r _ _ ab)).
interpretation "Or_intro_l_ko_2" 'Or_intro_l_ko_2 a ab =
(cast _ _ (show ab (cast _ _ (Or_intro_l _ _ a)))).
-notation < "\infrule hbox(\emsp a \emsp) ab (∨\sub(\i_\l))" with precedence 19
+notation < "maction (\infrule hbox(\emsp a \emsp) ab (∨\sub(\i_\l))) (\vdots)" with precedence 19
for @{ 'Or_intro_l_ok_1 $a $ab }.
interpretation "Or_intro_l_ok_1" 'Or_intro_l_ok_1 a ab =
(show ab (Or_intro_l _ _ a)).
interpretation "Or_intro_r_ko_2" 'Or_intro_r_ko_2 a ab =
(cast _ _ (show ab (cast _ _ (Or_intro_r _ _ a)))).
-notation < "\infrule hbox(\emsp a \emsp) ab (∨\sub(\i_\r))" with precedence 19
+notation < "maction (\infrule hbox(\emsp a \emsp) ab (∨\sub(\i_\r))) (\vdots)" with precedence 19
for @{ 'Or_intro_r_ok_1 $a $ab }.
interpretation "Or_intro_r_ok_1" 'Or_intro_r_ok_1 a ab =
(show ab (Or_intro_r _ _ a)).
interpretation "Or_elim_ko_2" 'Or_elim_ko_2 ab \eta.ac \eta.bc c =
(cast _ _ (show c (cast _ _ (Or_elim _ _ _ (cast _ _ ab) (cast _ _ ac) (cast _ _ bc))))).
-notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) c (∨\sub\e \emsp ident Ha \emsp ident Hb)" with precedence 19
+notation < "maction (\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) c (∨\sub\e \emsp ident Ha \emsp ident Hb)) (\vdots)" with precedence 19
for @{ 'Or_elim_ok_1 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }.
interpretation "Or_elim_ok_1" 'Or_elim_ok_1 ab \eta.ac \eta.bc c =
(show c (Or_elim _ _ _ ab ac bc)).
interpretation "Top_intro_ko_2" 'Top_intro_ko_2 =
(cast _ _ (show _ (cast _ _ Top_intro))).
-notation < "\infrule \nbsp ⊤ (⊤\sub\i)" with precedence 19
+notation < "maction (\infrule \nbsp ⊤ (⊤\sub\i)) (\vdots)" with precedence 19
for @{'Top_intro_ok_1}.
interpretation "Top_intro_ok_1" 'Top_intro_ok_1 = (show _ Top_intro).
-notation < "\infrule \nbsp ⊤ (⊤\sub\i)" with precedence 19
+notation < "maction (\infrule \nbsp ⊤ (⊤\sub\i)) (\vdots)" with precedence 19
for @{'Top_intro_ok_2 }.
interpretation "Top_intro_ok_2" 'Top_intro_ok_2 = (cast _ _ (show _ Top_intro)).
interpretation "Bot_elim_ko_2" 'Bot_elim_ko_2 a b =
(cast _ _ (show a (Bot_elim _ (cast _ _ b)))).
-notation < "\infrule b a (⊥\sub\e)" with precedence 19
+notation < "maction (\infrule b a (⊥\sub\e)) (\vdots)" with precedence 19
for @{'Bot_elim_ok_1 $a $b}.
interpretation "Bot_elim_ok_1" 'Bot_elim_ok_1 a b =
(show a (Bot_elim _ b)).
interpretation "Not_intro_ko_2" 'Not_intro_ko_2 ab \eta.b =
(cast _ _ (show ab (cast _ _ (Not_intro _ (cast _ _ b))))).
-notation < "\infrule hbox(\emsp b \emsp) ab (\lnot\sub(\emsp\i) \emsp ident H) " with precedence 19
+notation < "maction (\infrule hbox(\emsp b \emsp) ab (\lnot\sub(\emsp\i) \emsp ident H) ) (\vdots)" with precedence 19
for @{ 'Not_intro_ok_1 $ab (λ${ident H}:$p.$b) }.
interpretation "Not_intro_ok_1" 'Not_intro_ok_1 ab \eta.b =
(show ab (Not_intro _ b)).
interpretation "Not_elim_ko_2" 'Not_elim_ko_2 ab a b =
(cast _ _ (show b (cast _ _ (Not_elim _ (cast _ _ ab) (cast _ _ a))))).
-notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (\lnot\sub(\emsp\e)) " with precedence 19
+notation < "maction (\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (\lnot\sub(\emsp\e)) ) (\vdots)" with precedence 19
for @{ 'Not_elim_ok_1 $ab $a $b }.
interpretation "Not_elim_ok_1" 'Not_elim_ok_1 ab a b =
(show b (Not_elim _ ab a)).
interpretation "RAA_ko_2" 'RAA_ko_2 Px Pn =
(cast _ _ (show Pn (cast _ _ (Raa _ (cast _ _ Px))))).
-notation < "\infrule hbox(\emsp Px \emsp) Pn (\RAA \emsp ident x)" with precedence 19
+notation < "maction (\infrule hbox(\emsp Px \emsp) Pn (\RAA \emsp ident x)) (\vdots)" with precedence 19
for @{ 'RAA_ok_1 (λ${ident x}:$tx.$Px) $Pn }.
interpretation "RAA_ok_1" 'RAA_ok_1 Px Pn =
(show Pn (Raa _ Px)).
interpretation "Exists_intro_ko_2" 'Exists_intro_ko_2 Pn Px =
(cast _ _ (show Px (cast _ _ (Exists_intro _ _ _ (cast _ _ Pn))))).
-notation < "\infrule hbox(\emsp Pn \emsp) Px (∃\sub\i)" with precedence 19
+notation < "maction (\infrule hbox(\emsp Pn \emsp) Px (∃\sub\i)) (\vdots)" with precedence 19
for @{ 'Exists_intro_ok_1 $Pn $Px }.
interpretation "Exists_intro_ok_1" 'Exists_intro_ok_1 Pn Px =
(show Px (Exists_intro _ _ _ Pn)).
interpretation "Exists_elim_ko_2" 'Exists_elim_ko_2 ExPx Pc c =
(cast _ _ (show c (cast _ _ (Exists_elim _ _ _ (cast _ _ ExPx) (cast _ _ Pc))))).
-notation < "\infrule hbox(\emsp ExPx \emsp\emsp\emsp Pc \emsp) c (∃\sub\e \emsp ident n \emsp ident HPn)" with precedence 19
+notation < "maction (\infrule hbox(\emsp ExPx \emsp\emsp\emsp Pc \emsp) c (∃\sub\e \emsp ident n \emsp ident HPn)) (\vdots)" with precedence 19
for @{ 'Exists_elim_ok_1 $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }.
interpretation "Exists_elim_ok_1" 'Exists_elim_ok_1 ExPx Pc c =
(show c (Exists_elim _ _ _ ExPx Pc)).
interpretation "Forall_intro_ko_2" 'Forall_intro_ko_2 Px Pn =
(cast _ _ (show Pn (cast _ _ (Forall_intro _ _ (cast _ _ Px))))).
-notation < "\infrule hbox(\emsp Px \emsp) Pn (∀\sub\i \emsp ident x)" with precedence 19
+notation < "maction (\infrule hbox(\emsp Px \emsp) Pn (∀\sub\i \emsp ident x)) (\vdots)" with precedence 19
for @{ 'Forall_intro_ok_1 (λ${ident x}:$tx.$Px) $Pn }.
interpretation "Forall_intro_ok_1" 'Forall_intro_ok_1 Px Pn =
(show Pn (Forall_intro _ _ Px)).
interpretation "Forall_elim_ko_2" 'Forall_elim_ko_2 Px Pn =
(cast _ _ (show Pn (cast _ _ (Forall_elim _ _ _ (cast _ _ Px))))).
-notation < "\infrule hbox(\emsp Px \emsp) Pn (∀\sub\e)" with precedence 19
+notation < "maction (\infrule hbox(\emsp Px \emsp) Pn (∀\sub\e)) (\vdots)" with precedence 19
for @{ 'Forall_elim_ok_1 $Px $Pn }.
interpretation "Forall_elim_ok_1" 'Forall_elim_ok_1 Px Pn =
(show Pn (Forall_elim _ _ _ Px)).
projects / helm.git / blobdiff