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 inductive Prod (A,B:Type[0]) : Type[0] ≝
22 pair : A → B → Prod A B.
24 interpretation "Pair construction" 'pair x y = (pair ? ? x y).
26 interpretation "Product" 'product x y = (Prod x y).
28 definition fst ≝ λA,B.λp:A × B.
29 match p with [pair a b ⇒ a].
31 definition snd ≝ λA,B.λp:A × B.
32 match p with [pair a b ⇒ b].
34 interpretation "pair pi1" 'pi1 = (fst ? ?).
35 interpretation "pair pi2" 'pi2 = (snd ? ?).
36 interpretation "pair pi1" 'pi1a x = (fst ? ? x).
37 interpretation "pair pi2" 'pi2a x = (snd ? ? x).
38 interpretation "pair pi1" 'pi1b x y = (fst ? ? x y).
39 interpretation "pair pi2" 'pi2b x y = (snd ? ? x y).
41 theorem eq_pair_fst_snd: ∀A,B.∀p:A × B.
42 p = 〈 \fst p, \snd p 〉.
43 #A #B #p (cases p) // qed.
46 inductive Sum (A,B:Type[0]) : Type[0] ≝
50 interpretation "Disjoint union" 'plus A B = (Sum A B).
53 inductive option (A:Type[0]) : Type[0] ≝
55 | Some : A → option A.
58 inductive Sig (A:Type[0]) (f:A→Type[0]) : Type[0] ≝
59 dp: ∀a:A.(f a)→Sig A f.
61 interpretation "Sigma" 'sigma x = (Sig ? x).