(* Progetto FreeScale *)
(* *)
(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Sviluppo: 2008-2010 *)
+(* Ultima modifica: 05/08/2009 *)
(* *)
(* ********************************************************************** *)
-include "common/theory.ma".
-
(* coppia dipendente *)
-ninductive sigma (A:Type) (P:A → Type) : Type ≝
+inductive 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).
-ndefinition sigmaFst ≝
+definition sigmaFst ≝
λT:Type.λf:T → Type.λs:sigma T f.match s with [ sigma_intro x _ ⇒ x ].
-ndefinition sigmaSnd ≝
+definition sigmaSnd ≝
λT:Type.λf:T → Type.λs:sigma T f.match s return λs.f (sigmaFst ?? s) with [ sigma_intro _ x ⇒ x ].