(* Progetto FreeScale *)
(* *)
(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Ultima modifica: 05/08/2009 *)
+(* Sviluppo: 2008-2010 *)
(* *)
(* ********************************************************************** *)
+include "common/theory.ma".
+
(* coppia dipendente *)
-inductive sigma (A:Type) (P:A → Type) : Type ≝
+ninductive sigma (A:Type) (P:A → Type) : Type ≝
sigma_intro: ∀x:A.P x → sigma A P.
notation < "hvbox(\Sigma ident i opt (: tx) break . p)"
interpretation "sigma" 'Sigma \eta.x = (sigma ? x).
-definition sigmaFst ≝
+ndefinition sigmaFst ≝
λT:Type.λf:T → Type.λs:sigma T f.match s with [ sigma_intro x _ ⇒ x ].
-definition sigmaSnd ≝
+ndefinition sigmaSnd ≝
λT:Type.λf:T → Type.λs:sigma T f.match s return λs.f (sigmaFst ?? s) with [ sigma_intro _ x ⇒ x ].