Left : A → Or A B
| Right : B → Or A B.
-interpretation "constructive or" 'or x y =
- (cic:/matita/constructive_connectives/Or.ind#xpointer(1/1) x y).
+interpretation "constructive or" 'or x y = (Or x y).
inductive And (A,B:Type) : Type ≝
| Conj : A → B → And A B.
-interpretation "constructive and" 'and x y =
- (cic:/matita/constructive_connectives/And.ind#xpointer(1/1) x y).
+interpretation "constructive and" 'and x y = (And x y).
inductive exT (A:Type) (P:A→Type) : Type ≝
ex_introT: ∀w:A. P w → exT A P.
@{\lambda ${ident i} . $p}}}.
*)
-interpretation "constructive exists" 'exists \eta.x =
- (cic:/matita/constructive_connectives/ex.ind#xpointer(1/1) _ x).
-interpretation "constructive exists (Type)" 'exists \eta.x =
- (cic:/matita/constructive_connectives/exT.ind#xpointer(1/1) _ x).
+interpretation "constructive exists" 'exists \eta.x = (ex ? x).
+interpretation "constructive exists (Type)" 'exists \eta.x = (exT ? x).
alias id "False" = "cic:/matita/logic/connectives/False.ind#xpointer(1/1)".
definition Not ≝ λx:Type.x → False.
-interpretation "constructive not" 'not x =
- (cic:/matita/constructive_connectives/Not.con x).
+interpretation "constructive not" 'not x = (Not x).