More test files

Author: nomeata

tests/lean/run/issue10431.lean

@@ -0,0 +1,24 @@
+inductive L (α : Type u) : Type u where
+  | nil : L α
+  | cons : α → L α → L α
+
+def L.eq [BEq α] (xs ys : L α) : Bool :=
+  match _ : xs.ctorIdx == ys.ctorIdx with
+  | false => false
+  | true =>
+    match xs, ys with
+    | .nil, .nil => true
+    | .cons x xs, .cons y ys => x == y && xs.eq ys
+
+/--
+info: theorem L.eq.eq_def.{u_1} : ∀ {α : Type u_1} [inst : BEq α] (xs ys : L α),
+  xs.eq ys =
+    match h : xs.ctorIdx == ys.ctorIdx with
+    | false => false
+    | true =>
+      match xs, ys, h with
+      | L.nil, L.nil, h => true
+      | L.cons x xs, L.cons y ys, h => x == y && xs.eq ys
+-/
+#guard_msgs in
+#print sig L.eq.eq_def

tests/lean/run/issue2962.lean

@@ -0,0 +1,51 @@
+inductive N where
+  | zero : N
+  | succ : N → N
+
+def replace (f : N → Option N) (t : N) : N :=
+  match f t with
+  | some u => u
+  | none =>
+    match t with
+    | .zero => .zero
+    | .succ t' => replace f t'
+
+/--
+info: equations:
+@[defeq] theorem replace.eq_1 : ∀ (f : N → Option N),
+  replace f N.zero =
+    match f N.zero with
+    | some u => u
+    | none => N.zero
+@[defeq] theorem replace.eq_2 : ∀ (f : N → Option N) (t' : N),
+  replace f t'.succ =
+    match f t'.succ with
+    | some u => u
+    | none => replace f t'
+-/
+#guard_msgs in
+#print equations replace
+
+def replace2 (f : N → Option N) (t1 t2 : N) : N :=
+  match f t1 with
+  | some u => u
+  | none =>
+    match t2 with
+    | .zero => .zero
+    | .succ t' => replace2 f t1 t'
+
+/--
+info: equations:
+@[defeq] theorem replace2.eq_1 : ∀ (f : N → Option N) (t1 : N),
+  replace2 f t1 N.zero =
+    match f t1 with
+    | some u => u
+    | none => N.zero
+@[defeq] theorem replace2.eq_2 : ∀ (f : N → Option N) (t1 t' : N),
+  replace2 f t1 t'.succ =
+    match f t1 with
+    | some u => u
+    | none => replace2 f t1 t'
+-/
+#guard_msgs in
+#print equations replace2

tests/lean/run/issue9846.lean

@@ -0,0 +1,21 @@
+def testMatch : Array α → Unit
+  | #[_] => ()
+  | _ => ()
+
+/--
+error: Failed to realize constant testMatch.match_1.eq_1:
+  failed to generate equality theorems for `match` expression `testMatch.match_1`
+  case isTrue
+  α✝ : Type u_1
+  motive✝ : Array α✝ → Sort u_2
+  x✝¹ : Array α✝
+  h_1✝ : (head : α✝) → motive✝ #[head]
+  h_2✝ : (x : Array α✝) → motive✝ x
+  x✝ : ∀ (head : α✝), x✝¹ = #[head] → False
+  h✝ : x✝¹.size = 1
+  ⊢ (⋯ ▸ fun h => ⋯ ▸ h_1✝ (x✝¹.getLit 0 ⋯ ⋯)) ⋯ = h_2✝ x✝¹
+---
+error: Unknown constant `testMatch.match_1.eq_1`
+-/
+#guard_msgs in
+#print testMatch.match_1.eq_1