(* *)
(**************************************************************************)
-include "ground_2/lib/list2.ma".
+include "ground_2/notation/constructors/diamond_0.ma".
+include "ground_2/notation/constructors/semicolon_3.ma".
+include "ground_2/lib/arith.ma".
(* MULTIPLE RELOCATION WITH PAIRS *******************************************)
-definition mr2: Type[0] ≝ list2 nat nat.
+inductive mr2: Type[0] :=
+ | nil2 : mr2
+ | cons2: nat → nat → mr2 → mr2.
+
+interpretation "nil (multiple relocation with pairs)"
+ 'Diamond = (nil2).
+
+interpretation "cons (multiple relocation with pairs)"
+ 'Semicolon hd1 hd2 tl = (cons2 hd1 hd2 tl).