X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Ftypes.ma;h=08b99a8cb552165d09f203353a95c77625ac45c2;hb=a64572b00ce40f476577bf827488d23ddf763120;hp=c14cc60b4bf4f32ef21f34965932982f2fafdc44;hpb=53452958508001e7af3090695b619fe92135fb9e;p=helm.git

diff --git a/matita/matita/lib/basics/types.ma b/matita/matita/lib/basics/types.ma
index c14cc60b4..08b99a8cb 100644
--- a/matita/matita/lib/basics/types.ma
+++ b/matita/matita/lib/basics/types.ma
@@ -56,4 +56,6 @@ inductive option (A:Type[0]) : Type[0] ≝
 
 (* sigma *)
 inductive Sig (A:Type[0]) (f:A→Type[0]) : Type[0] ≝
-  dp: ∀a:A.(f a)→Sig A f.
\ No newline at end of file
+  dp: ∀a:A.(f a)→Sig A f.
+  
+interpretation "Sigma" 'sigma x = (Sig ? x).