(* *)
(**************************************************************************)
+(* STATO: COMPILA *)
+
(* Project started Wed Oct 12, 2005 ***************************************)
set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/class_defs".
(cic:/matita/PREDICATIVE-TOPOLOGY/class_defs/call.ind#xpointer(1/1) _ x).
notation > "hvbox(\xforall ident i opt (: ty) break . p)"
- right associative with precedence 20
+ with precedence 20
for @{ 'xforall ${default
@{\lambda ${ident i} : $ty. $p}
@{\lambda ${ident i} . $p}}}.
(cic:/matita/PREDICATIVE-TOPOLOGY/class_defs/call2.ind#xpointer(1/1) _ _ x y).
notation > "hvbox(\xforall ident i1 opt (: ty1) ident i2 opt (: ty2) break . p)"
- right associative with precedence 20
+ with precedence 20
for @{ 'xforall2 ${default
@{\lambda ${ident i1} : $ty1. \lambda ${ident i2} : $ty2. $p}
@{\lambda ${ident i1}, ${ident i2}. $p}}}.