Pairs are now records.

[helm.git] / matita / matita / lib / basics / types.ma

diff --git a/matita/matita/lib/basics/types.ma b/matita/matita/lib/basics/types.ma
index f35dde531e5fe93debc3f5b0e54ebb78c8f9425b..2852662e448f2e9076f24ca08f23932a6b749779 100644 (file)
--- a/matita/matita/lib/basics/types.ma
+++ b/matita/matita/lib/basics/types.ma
@@ -18,19 +18,15 @@ inductive void : Type[0] ≝.
 inductive unit : Type[0] ≝ it: unit.
 
 (* Prod *)
-inductive Prod (A,B:Type[0]) : Type[0] ≝
-pair : A → B → Prod A B.
+record Prod (A,B:Type[0]) : Type[0] ≝ {
+   fst: A
+ ; snd: B
+ }.
 
-interpretation "Pair construction" 'pair x y = (pair ? ? x y).
+interpretation "Pair construction" 'pair x y = (mk_Prod ? ? x y).
 
 interpretation "Product" 'product x y = (Prod x y).
 
-definition fst ≝ λA,B.λp:A × B.
-  match p with [pair a b ⇒ a]. 
-
-definition snd ≝ λA,B.λp:A × B.
-  match p with [pair a b ⇒ b].
-
 interpretation "pair pi1" 'pi1 = (fst ? ?).
 interpretation "pair pi2" 'pi2 = (snd ? ?).
 interpretation "pair pi1" 'pi1a x = (fst ? ? x).