2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department of the University of Bologna, Italy.
8 \ / This file is distributed under the terms of the
9 \ / GNU General Public License Version 2
10 V_______________________________________________________________ *)
12 include "basics/logic.ma".
15 inductive void : Type[0] ≝.
18 inductive unit : Type[0] ≝ it: unit.
21 record Prod (A,B:Type[0]) : Type[0] ≝ {
26 interpretation "Pair construction" 'pair x y = (mk_Prod ? ? x y).
28 interpretation "Product" 'product x y = (Prod x y).
30 interpretation "pair pi1" 'pi1 = (fst ? ?).
31 interpretation "pair pi2" 'pi2 = (snd ? ?).
32 interpretation "pair pi1" 'pi1a x = (fst ? ? x).
33 interpretation "pair pi2" 'pi2a x = (snd ? ? x).
34 interpretation "pair pi1" 'pi1b x y = (fst ? ? x y).
35 interpretation "pair pi2" 'pi2b x y = (snd ? ? x y).
37 theorem eq_pair_fst_snd: ∀A,B.∀p:A × B.
38 p = 〈 \fst p, \snd p 〉.
39 #A #B #p (cases p) // qed.
41 lemma fst_eq : ∀A,B.∀a:A.∀b:B. \fst 〈a,b〉 = a.
44 lemma snd_eq : ∀A,B.∀a:A.∀b:B. \snd 〈a,b〉 = b.
48 inductive Sum (A,B:Type[0]) : Type[0] ≝
52 interpretation "Disjoint union" 'plus A B = (Sum A B).
55 inductive option (A:Type[0]) : Type[0] ≝
57 | Some : A → option A.
60 inductive Sig (A:Type[0]) (f:A→Type[0]) : Type[0] ≝
61 dp: ∀a:A.(f a)→Sig A f.
63 interpretation "Sigma" 'sigma x = (Sig ? x).