(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/demo/realisability/".
-
include "logic/connectives.ma".
include "datatypes/constructors.ma".
match s return λs.P (pi1 ? ? s) with
[ sigma_intro _ p ⇒ p].
-notation "hvbox(Σ ident i opt (: ty) break . p)"
+notation "hvbox(\Sigma ident i opt (: ty) break . p)"
right associative with precedence 20
for @{ 'sigma ${default
@{\lambda ${ident i} : $ty. $p}
@{\lambda ${ident i} . $p}}}.
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "Sigma" 'sigma \eta.x =
- (cic:/matita/demo/realisability/sigma.ind#xpointer(1/1) _ x).
+interpretation "Sigma" 'sigma \eta.x = (sigma ? x).
let rec type_OF_SP F ≝
match F return λF.Type with