commit by user andrea

[helm.git] / weblib / basics / types.ma

diff --git a/weblib/basics/types.ma b/weblib/basics/types.ma
index 494177cfc11058555764c44e6a9a619e3fe0e27d..586ce31ce7bb527d251d3d1a9ddf5704f9163a2a 100644 (file)
--- 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).
\ No newline at end of file