1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "logic/connectives.ma".
17 inductive Or (A,B:Type) : Type ≝
21 interpretation "constructive or" 'or x y =
22 (cic:/matita/constructive_connectives/Or.ind#xpointer(1/1) x y).
24 inductive And (A,B:Type) : Type ≝
25 | Conj : A → B → And A B.
27 interpretation "constructive and" 'and x y =
28 (cic:/matita/constructive_connectives/And.ind#xpointer(1/1) x y).
30 inductive exT (A:Type) (P:A→Type) : Type ≝
31 ex_introT: ∀w:A. P w → exT A P.
33 inductive ex (A:Type) (P:A→Prop) : Type ≝
34 ex_intro: ∀w:A. P w → ex A P.
37 notation < "hvbox(Σ ident i opt (: ty) break . p)"
38 right associative with precedence 20
39 for @{ 'sigma ${default
40 @{\lambda ${ident i} : $ty. $p)}
41 @{\lambda ${ident i} . $p}}}.
44 interpretation "constructive exists" 'exists \eta.x =
45 (cic:/matita/constructive_connectives/ex.ind#xpointer(1/1) _ x).
46 interpretation "constructive exists (Type)" 'exists \eta.x =
47 (cic:/matita/constructive_connectives/exT.ind#xpointer(1/1) _ x).
49 alias id "False" = "cic:/matita/logic/connectives/False.ind#xpointer(1/1)".
50 definition Not ≝ λx:Type.x → False.
52 interpretation "constructive not" 'not x =
53 (cic:/matita/constructive_connectives/Not.con x).