(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/RELATIONAL/datatypes/List".
+
include "preamble.ma".
-inductive List (A:Set): Set \def
+inductive List (A: Type): Type \def
| nil: List A
| cons: List A \to A \to List A
.
(*CSC: the URI must disappear: there is a bug now *)
interpretation "nil" 'nil =
- (cic:/matita/RELATIONAL/datatypes/List/List.ind#xpointer(1/1) _).
+ (cic:/matita/RELATIONAL/datatypes/List/List.ind#xpointer(1/1) ?).
notation "hvbox([])"
non associative with precedence 95
(*CSC: the URI must disappear: there is a bug now *)
interpretation "right cons" 'rcons x y =
- (cic:/matita/RELATIONAL/datatypes/List/List.ind#xpointer(1/2) _ x y).
+ (cic:/matita/RELATIONAL/datatypes/List/List.ind#xpointer(1/2) ? x y).
notation "hvbox([a break @ b])"
non associative with precedence 95