X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Ftypes.ma;h=2852662e448f2e9076f24ca08f23932a6b749779;hb=bf5696fc20ffbe552ecb1cd8af0d6fc78d1de9e8;hp=f35dde531e5fe93debc3f5b0e54ebb78c8f9425b;hpb=da5cf21f33e7303bf9b1fc60470de1f6101714dd;p=helm.git

diff --git a/matita/matita/lib/basics/types.ma b/matita/matita/lib/basics/types.ma
index f35dde531..2852662e4 100644
--- 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).