X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Fbasics%2Ftypes.ma;h=0fd4eb5886cb0d067459a47b9c5703c5b48e413e;hb=0bf47116203bc07de95643f389e228e0d59cab6b;hp=494177cfc11058555764c44e6a9a619e3fe0e27d;hpb=cf367920b94b3a95c5c068c2f0672b97bf579731;p=helm.git

diff --git a/weblib/basics/types.ma b/weblib/basics/types.ma
index 494177cfc..0fd4eb588 100644
--- a/weblib/basics/types.ma
+++ b/weblib/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).