test: inductive types for testing SizeOf.lean

tests/lean/run/sizeof1.lean

@@ -0,0 +1,14 @@
+mutual
+
+inductive TreePos (α : Type u) (β : Type v) where
+  | leaf (a : α)
+  | node (children : List (List (TreeNeg α β)))
+
+inductive TreeNeg (α : Type u) (β : Type v) where
+  | leaf (a : β)
+  | node (children : List (List (TreePos α β)))
+
+end
+
+#print TreePos.leaf.sizeOf_spec
+#print TreePos.node.sizeOf_spec

tests/lean/run/sizeof2.lean

@@ -0,0 +1,12 @@
+mutual
+
+  inductive Arg (α : Type u) where
+    | val  (a : α)
+    | expr (e : Expr α)
+
+  inductive Expr (α : Type u) where
+    | app (f : String) (a : List (Arg α))
+
+end
+
+#print Expr.app.sizeOf_spec

tests/lean/run/sizeof3.lean

@@ -0,0 +1,23 @@
+set_option trace.Meta.sizeOf true in
+mutual
+  inductive AList (α β : Type u)
+    | nil
+    | cons (a : α) (t : BList α β)
+
+  inductive BList (α β : Type u)
+    | cons (b : β) (t : AList α β)
+end
+
+#print AList.nil.sizeOf_spec
+#print AList.cons.sizeOf_spec
+#print BList.cons.sizeOf_spec
+
+mutual
+  inductive Foo (α : Type u)
+    | mk (cs : AList (Foo α) (Boo α))
+
+  inductive Boo (α : Type u)
+    | mk (a : α) (cs : BList (Foo α) (Boo α))
+end
+
+#print Boo.mk.sizeOf_spec

tests/lean/run/sizeof4.lean

@@ -0,0 +1,14 @@
+inductive Foo (β : Type u) : Sort v → Type (max u v)
+  | mk {α : Sort v} (b : β) (a : α) : Foo β α
+
+inductive Bla (α : Type u) : Type (u+1) where
+  | mk₁ (x : Foo (Bla α) Nat)
+  | mk₂ (n m : Nat) (x : Foo (Bla α) (n = m))
+
+#print Bla.rec
+
+#print Bla._sizeOf_1
+#print Bla._sizeOf_2
+#print Bla._sizeOf_3
+#print Bla.mk₁.sizeOf_spec
+#print Bla.mk₂.sizeOf_spec

tests/lean/run/sizeof5.lean

@@ -0,0 +1,10 @@
+inductive Vec (α : Type u) : Nat → Type u where
+  | nil  : Vec α 0
+  | cons : α → {n : Nat} → Vec α n → Vec α (n+1)
+
+inductive Expr where
+  | app2 (f : String) (args : Vec Expr 2)
+  | app3 (f : String) (args : Vec Expr 3)
+
+#print Expr.app2.sizeOf_spec
+#print Expr.app3.sizeOf_spec