diff --git a/src/Lean/EqnCompiler.lean b/src/Lean/EqnCompiler.lean
index 4a52198eaa..b422cdba03 100644
--- a/src/Lean/EqnCompiler.lean
+++ b/src/Lean/EqnCompiler.lean
@@ -4,3 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.EqnCompiler.MatchPattern
+import Lean.EqnCompiler.DepElim
diff --git a/tmp/eqns/prototype2.lean b/src/Lean/EqnCompiler/DepElim.lean
similarity index 70%
rename from tmp/eqns/prototype2.lean
rename to src/Lean/EqnCompiler/DepElim.lean
index 4c3295515b..7036c8d051 100644
--- a/tmp/eqns/prototype2.lean
+++ b/src/Lean/EqnCompiler/DepElim.lean
@@ -1,3 +1,8 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
 import Lean.Util.CollectLevelParams
 import Lean.Meta.Check
 import Lean.Meta.Tactic.Cases
@@ -560,284 +565,3 @@ withAlts motive lhss fun alts minors => do
 end DepElim
 end Meta
 end Lean
-
-open Lean
-open Lean.Meta
-open Lean.Meta.DepElim
-
-/- Infrastructure for testing -/
-
-universes u v
-
-def inaccessible {α : Sort u} (a : α) : α := a
-def val {α : Sort u} (a : α) : α := a
-
-private def getConstructorVal (ctorName : Name) (fn : Expr) (args : Array Expr) : MetaM (Option (ConstructorVal × Expr × Array Expr)) := do
-env ← getEnv;
-match env.find? ctorName with
-| some (ConstantInfo.ctorInfo v) => if args.size == v.nparams + v.nfields then pure $ some (v, fn, args) else pure none
-| _                              => pure none
-
-private def constructorApp? (e : Expr) : MetaM (Option (ConstructorVal × Expr × Array Expr)) := do
-env ← getEnv;
-match e with
-| Expr.lit (Literal.natVal n) _ =>
-   if n == 0 then getConstructorVal `Nat.zero (mkConst `Nat.zero) #[] else getConstructorVal `Nat.succ (mkConst `Nat.succ) #[mkNatLit (n-1)]
-| _ =>
-  let fn := e.getAppFn;
-  match fn with
-  | Expr.const n _ _ => getConstructorVal n fn e.getAppArgs
-  | _                => pure none
-
-/- Convert expression using auxiliary hints `inaccessible` and `val` into a pattern -/
-partial def mkPattern : Expr → MetaM Pattern
-| e =>
-  if e.isAppOfArity `val 2 then
-    pure $ Pattern.val Syntax.missing e.appArg!
-  else if e.isAppOfArity `inaccessible 2 then
-    pure $ Pattern.inaccessible Syntax.missing e.appArg!
-  else if e.isFVar then
-    pure $ Pattern.var Syntax.missing e.fvarId!
-  else match e.arrayLit? with
-    | some es => do
-      pats ← es.mapM mkPattern;
-      type ← inferType e;
-      type ← whnfD type;
-      let elemType := type.appArg!;
-      pure $ Pattern.arrayLit Syntax.missing elemType pats
-    | none => do
-      e ← whnfD e;
-      r? ← constructorApp? e;
-      match r? with
-      | none      => throw $ Exception.other "unexpected pattern"
-      | some (cval, fn, args) => do
-        let params := args.extract 0 cval.nparams;
-        let fields := args.extract cval.nparams args.size;
-        pats ← fields.toList.mapM mkPattern;
-        pure $ Pattern.ctor Syntax.missing cval.name fn.constLevels! params.toList pats
-
-partial def decodePats : Expr → MetaM (List Pattern)
-| e =>
-  match e.app2? `Pat with
-  | some (_, pat) => do pat ← mkPattern pat; pure [pat]
-  | none =>
-    match e.prod? with
-    | none => throw $ Exception.other "unexpected pattern"
-    | some (pat, pats) => do
-      pat  ← decodePats pat;
-      pats ← decodePats pats;
-      pure (pat ++ pats)
-
-partial def decodeAltLHS (e : Expr) : MetaM AltLHS :=
-forallTelescopeReducing e fun args body => do
-  decls ← args.toList.mapM (fun arg => getLocalDecl arg.fvarId!);
-  pats  ← decodePats body;
-  pure { fvarDecls := decls, patterns := pats }
-
-partial def decodeAltLHSs : Expr → MetaM (List AltLHS)
-| e =>
-  match e.app2? `LHS with
-  | some (_, lhs) => do lhs ← decodeAltLHS lhs; pure [lhs]
-  | none =>
-    match e.prod? with
-    | none => throw $ Exception.other "unexpected LHS"
-    | some (lhs, lhss) => do
-      lhs  ← decodeAltLHSs lhs;
-      lhss ← decodeAltLHSs lhss;
-      pure (lhs ++ lhss)
-
-def withDepElimFrom {α} (declName : Name) (numPats : Nat) (k : List FVarId → List AltLHS → MetaM α) : MetaM α := do
-cinfo ← getConstInfo declName;
-forallTelescopeReducing cinfo.type fun args body =>
-  if args.size < numPats then
-    throw $ Exception.other "insufficient number of parameters"
-  else do
-    let xs := (args.extract (args.size - numPats) args.size).toList.map $ Expr.fvarId!;
-    alts ← decodeAltLHSs body;
-    k xs alts
-
-inductive Pat {α : Sort u} (a : α) : Type u
-| mk : Pat
-
-inductive LHS {α : Sort u} (a : α) : Type u
-| mk : LHS
-
-instance LHS.inhabited {α} (a : α) : Inhabited (LHS a) := ⟨LHS.mk⟩
-
--- set_option trace.Meta.debug true
--- set_option trace.Meta.Tactic.cases true
--- set_option trace.Meta.Tactic.subst true
-
-@[init] def register : IO Unit :=
-registerTraceClass `Meta.mkElim
-
-def test (ex : Name) (numPats : Nat) (elimName : Name) (inProp : Bool := false) : MetaM Unit :=
-withDepElimFrom ex numPats fun majors alts => do
-  let majors := majors.map mkFVar;
-  trace! `Meta.debug ("majors: " ++ majors.toArray);
-  r ← mkElim elimName majors alts inProp;
-  unless r.counterExamples.isEmpty $
-    throwOther ("missing cases:" ++ Format.line ++ counterExamplesToMessageData r.counterExamples);
-  unless r.unusedAltIdxs.isEmpty $
-    throwOther ("unused alternatives: " ++ toString (r.unusedAltIdxs.map fun idx => "#" ++ toString (idx+1)));
-  pure ()
-
-def ex0 (x : Nat) : LHS (forall (y : Nat), Pat y)
-:= arbitrary _
-
-#eval test `ex0 1 `elimTest0
-#print elimTest0
-
-def ex1 (α : Type u) (β : Type v) (n : Nat) (x : List α) (y : List β) :
-  LHS (Pat ([] : List α) × Pat ([] : List β))
-× LHS (forall (a : α) (as : List α) (b : β) (bs : List β), Pat (a::as) × Pat (b::bs))
-× LHS (forall (a : α) (as : List α), Pat (a::as) × Pat ([] : List β))
-× LHS (forall (b : β) (bs : List β), Pat ([] : List α) × Pat (b::bs))
-:= arbitrary _
-
-#eval test `ex1 2 `elimTest1
-#print elimTest1
-
-inductive Vec (α : Type u) : Nat → Type u
-| nil            : Vec 0
-| cons {n : Nat} : α → Vec n → Vec (n+1)
-
-def ex2 (α : Type u) (n : Nat) (xs : Vec α n) (ys : Vec α n) :
-  LHS (Pat (inaccessible 0) × Pat (Vec.nil : Vec α 0) × Pat (Vec.nil : Vec α 0))
-× LHS (forall (n : Nat) (x : α) (xs : Vec α n) (y : α) (ys : Vec α n), Pat (inaccessible (n+1)) × Pat (Vec.cons x xs) × Pat (Vec.cons y ys)) :=
-arbitrary _
-
-#eval test `ex2 3 `elimTest2
-#print elimTest2
-
-def ex3 (α : Type u) (β : Type v) (n : Nat) (x : List α) (y : List β) :
-  LHS (Pat ([] : List α) × Pat ([] : List β))
-× LHS (forall (a : α) (b : β), Pat [a] × Pat [b])
-× LHS (forall (a₁ a₂ : α) (as : List α) (b₁ b₂ : β) (bs : List β), Pat (a₁::a₂::as) × Pat (b₁::b₂::bs))
-× LHS (forall (as : List α) (bs : List β), Pat as × Pat bs)
-:= arbitrary _
-
-#eval test `ex3 2 `elimTest3
-#print elimTest3
-
-def ex4 (α : Type u) (n : Nat) (xs : Vec α n) :
-  LHS (Pat (inaccessible 0) × Pat (Vec.nil : Vec α 0))
-× LHS (forall (n : Nat) (xs : Vec α (n+1)), Pat (inaccessible (n+1)) × Pat xs) :=
-arbitrary _
-
-#eval test `ex4 2 `elimTest4
-#print elimTest4
-
-def ex5 (α : Type u) (n : Nat) (xs : Vec α n) :
-  LHS (Pat Nat.zero × Pat (Vec.nil : Vec α 0))
-× LHS (forall (n : Nat) (xs : Vec α (n+1)), Pat (Nat.succ n) × Pat xs) :=
-arbitrary _
-
-#eval test `ex5 2 `elimTest5
-#print elimTest5
-
-def ex6 (α : Type u) (n : Nat) (xs : Vec α n) :
-  LHS (Pat (inaccessible Nat.zero) × Pat (Vec.nil : Vec α 0))
-× LHS (forall (N : Nat) (XS : Vec α N), Pat (inaccessible N) × Pat XS) :=
-arbitrary _
-
--- set_option trace.Meta.debug true
-
-#eval test `ex6 2 `elimTest6
-#print elimTest6
-
-def ex7 (α : Type u) (n : Nat) (xs : Vec α n) :
-  LHS (forall (a : α), Pat (inaccessible 1) × Pat (Vec.cons a Vec.nil))
-× LHS (forall (N : Nat) (XS : Vec α N), Pat (inaccessible N) × Pat XS) :=
-arbitrary _
-
-#eval test `ex7 2 `elimTest7
-#check elimTest7
-
-def isSizeOne {n : Nat} (xs : Vec Nat n) : Bool :=
-elimTest7 _ (fun _ _ => Bool) n xs (fun _ => true) (fun _ _ => false)
-
-#eval isSizeOne Vec.nil
-#eval isSizeOne (Vec.cons 1 Vec.nil)
-#eval isSizeOne (Vec.cons 2 (Vec.cons 1 Vec.nil))
-
-def singleton? {n : Nat} (xs : Vec Nat n) : Option Nat :=
-elimTest7 _ (fun _ _ => Option Nat) n xs (fun a => some a) (fun _ _ => none)
-
-#eval singleton? Vec.nil
-#eval singleton? (Vec.cons 10 Vec.nil)
-#eval singleton? (Vec.cons 20 (Vec.cons 10 Vec.nil))
-
-def ex8 (α : Type u) (n : Nat) (xs : Vec α n) :
-  LHS (forall (a b : α), Pat (inaccessible 2) × Pat (Vec.cons a (Vec.cons b Vec.nil)))
-× LHS (forall (N : Nat) (XS : Vec α N), Pat (inaccessible N) × Pat XS) :=
-arbitrary _
-
-#eval test `ex8 2 `elimTest8
-#print elimTest8
-
-def pair? {n : Nat} (xs : Vec Nat n) : Option (Nat × Nat) :=
-elimTest8 _ (fun _ _ => Option (Nat × Nat)) n xs (fun a b => some (a, b)) (fun _ _ => none)
-
-#eval pair? Vec.nil
-#eval pair? (Vec.cons 10 Vec.nil)
-#eval pair? (Vec.cons 20 (Vec.cons 10 Vec.nil))
-
-inductive Op : Nat → Nat → Type
-| mk : ∀ n, Op n n
-
-structure Node : Type :=
-(id₁ id₂ : Nat)
-(o : Op id₁ id₂)
-
-def ex9 (xs : List Node) :
-  LHS (forall (h : Node) (t : List Node), Pat (h :: Node.mk 1 1 (Op.mk 1) :: t))
-× LHS (forall (ys : List Node), Pat ys) :=
-arbitrary _
-
-#eval test `ex9 1 `elimTest9
-#print elimTest9
-
-def f (xs : List Node) : Bool :=
-elimTest9 (fun _ => Bool) xs
-  (fun _ _ => true)
-  (fun _   => false)
-
-#eval f []
-#eval f [⟨0, 0, Op.mk 0⟩]
-#eval f [⟨0, 0, Op.mk 0⟩, ⟨1, 1, Op.mk 1⟩]
-#eval f [⟨0, 0, Op.mk 0⟩, ⟨2, 2, Op.mk 2⟩]
-
-inductive Foo : Bool → Prop
-| bar : Foo false
-| baz : Foo false
-
-def ex10 (x : Bool) (y : Foo x) :
-  LHS (Pat (inaccessible false) × Pat Foo.bar)
-× LHS (forall (x : Bool) (y : Foo x), Pat (inaccessible x) × Pat y) :=
-arbitrary _
-
-#eval test `ex10 2 `elimTest10 true
-
-def ex11 (xs : List Node) :
-  LHS (forall (h : Node) (t : List Node), Pat (h :: Node.mk 1 1 (Op.mk 1) :: t))
-× LHS (Pat ([] : List Node)) :=
-arbitrary _
-
-#eval test `ex11 1 `elimTest11 -- should produce error message
-
-def ex12 (x y z : Bool) :
-  LHS (forall (x y : Bool), Pat x × Pat y    × Pat true)
-× LHS (forall (x z : Bool), Pat false × Pat true × Pat z)
-× LHS (forall (y z : Bool), Pat true × Pat false × Pat z) :=
-arbitrary _
-
-#eval test `ex12 3 `elimTest12 -- should produce error message
-
-def ex13 (xs : List Node) :
-  LHS (forall (h : Node) (t : List Node), Pat (h :: Node.mk 1 1 (Op.mk 1) :: t))
-× LHS (forall (ys : List Node), Pat ys)
-× LHS (forall (ys : List Node), Pat ys) :=
-arbitrary _
-
-#eval test `ex13 1 `elimTest13 -- should produce error message
diff --git a/tests/lean/run/depElim1.lean b/tests/lean/run/depElim1.lean
new file mode 100644
index 0000000000..cae677abdc
--- /dev/null
+++ b/tests/lean/run/depElim1.lean
@@ -0,0 +1,286 @@
+import Lean.EqnCompiler.DepElim
+
+open Lean
+open Lean.Meta
+open Lean.Meta.DepElim
+
+/- Infrastructure for testing -/
+
+universes u v
+
+def inaccessible {α : Sort u} (a : α) : α := a
+def val {α : Sort u} (a : α) : α := a
+
+private def getConstructorVal (ctorName : Name) (fn : Expr) (args : Array Expr) : MetaM (Option (ConstructorVal × Expr × Array Expr)) := do
+env ← getEnv;
+match env.find? ctorName with
+| some (ConstantInfo.ctorInfo v) => if args.size == v.nparams + v.nfields then pure $ some (v, fn, args) else pure none
+| _                              => pure none
+
+private def constructorApp? (e : Expr) : MetaM (Option (ConstructorVal × Expr × Array Expr)) := do
+env ← getEnv;
+match e with
+| Expr.lit (Literal.natVal n) _ =>
+   if n == 0 then getConstructorVal `Nat.zero (mkConst `Nat.zero) #[] else getConstructorVal `Nat.succ (mkConst `Nat.succ) #[mkNatLit (n-1)]
+| _ =>
+  let fn := e.getAppFn;
+  match fn with
+  | Expr.const n _ _ => getConstructorVal n fn e.getAppArgs
+  | _                => pure none
+
+/- Convert expression using auxiliary hints `inaccessible` and `val` into a pattern -/
+partial def mkPattern : Expr → MetaM Pattern
+| e =>
+  if e.isAppOfArity `val 2 then
+    pure $ Pattern.val Syntax.missing e.appArg!
+  else if e.isAppOfArity `inaccessible 2 then
+    pure $ Pattern.inaccessible Syntax.missing e.appArg!
+  else if e.isFVar then
+    pure $ Pattern.var Syntax.missing e.fvarId!
+  else match e.arrayLit? with
+    | some es => do
+      pats ← es.mapM mkPattern;
+      type ← inferType e;
+      type ← whnfD type;
+      let elemType := type.appArg!;
+      pure $ Pattern.arrayLit Syntax.missing elemType pats
+    | none => do
+      e ← whnfD e;
+      r? ← constructorApp? e;
+      match r? with
+      | none      => throw $ Exception.other "unexpected pattern"
+      | some (cval, fn, args) => do
+        let params := args.extract 0 cval.nparams;
+        let fields := args.extract cval.nparams args.size;
+        pats ← fields.toList.mapM mkPattern;
+        pure $ Pattern.ctor Syntax.missing cval.name fn.constLevels! params.toList pats
+
+partial def decodePats : Expr → MetaM (List Pattern)
+| e =>
+  match e.app2? `Pat with
+  | some (_, pat) => do pat ← mkPattern pat; pure [pat]
+  | none =>
+    match e.prod? with
+    | none => throw $ Exception.other "unexpected pattern"
+    | some (pat, pats) => do
+      pat  ← decodePats pat;
+      pats ← decodePats pats;
+      pure (pat ++ pats)
+
+partial def decodeAltLHS (e : Expr) : MetaM AltLHS :=
+forallTelescopeReducing e fun args body => do
+  decls ← args.toList.mapM (fun arg => getLocalDecl arg.fvarId!);
+  pats  ← decodePats body;
+  pure { fvarDecls := decls, patterns := pats }
+
+partial def decodeAltLHSs : Expr → MetaM (List AltLHS)
+| e =>
+  match e.app2? `LHS with
+  | some (_, lhs) => do lhs ← decodeAltLHS lhs; pure [lhs]
+  | none =>
+    match e.prod? with
+    | none => throw $ Exception.other "unexpected LHS"
+    | some (lhs, lhss) => do
+      lhs  ← decodeAltLHSs lhs;
+      lhss ← decodeAltLHSs lhss;
+      pure (lhs ++ lhss)
+
+def withDepElimFrom {α} (declName : Name) (numPats : Nat) (k : List FVarId → List AltLHS → MetaM α) : MetaM α := do
+cinfo ← getConstInfo declName;
+forallTelescopeReducing cinfo.type fun args body =>
+  if args.size < numPats then
+    throw $ Exception.other "insufficient number of parameters"
+  else do
+    let xs := (args.extract (args.size - numPats) args.size).toList.map $ Expr.fvarId!;
+    alts ← decodeAltLHSs body;
+    k xs alts
+
+inductive Pat {α : Sort u} (a : α) : Type u
+| mk : Pat
+
+inductive LHS {α : Sort u} (a : α) : Type u
+| mk : LHS
+
+instance LHS.inhabited {α} (a : α) : Inhabited (LHS a) := ⟨LHS.mk⟩
+
+-- set_option trace.Meta.debug true
+-- set_option trace.Meta.Tactic.cases true
+-- set_option trace.Meta.Tactic.subst true
+
+@[init] def register : IO Unit :=
+registerTraceClass `Meta.mkElim
+
+def test (ex : Name) (numPats : Nat) (elimName : Name) (inProp : Bool := false) : MetaM Unit :=
+withDepElimFrom ex numPats fun majors alts => do
+  let majors := majors.map mkFVar;
+  trace! `Meta.debug ("majors: " ++ majors.toArray);
+  r ← mkElim elimName majors alts inProp;
+  unless r.counterExamples.isEmpty $
+    throwOther ("missing cases:" ++ Format.line ++ counterExamplesToMessageData r.counterExamples);
+  unless r.unusedAltIdxs.isEmpty $
+    throwOther ("unused alternatives: " ++ toString (r.unusedAltIdxs.map fun idx => "#" ++ toString (idx+1)));
+  pure ()
+
+def testFailure (ex : Name) (numPats : Nat) (elimName : Name) (inProp : Bool := false) : MetaM Unit := do
+worked ← catch (do test ex numPats elimName inProp; pure true) (fun ex =>  _root_.dbgTrace ("ERROR: " ++ toString ex) fun _ => pure false);
+when worked $ throwOther "unexpected success"
+
+def ex0 (x : Nat) : LHS (forall (y : Nat), Pat y)
+:= arbitrary _
+
+#eval test `ex0 1 `elimTest0
+#print elimTest0
+
+def ex1 (α : Type u) (β : Type v) (n : Nat) (x : List α) (y : List β) :
+  LHS (Pat ([] : List α) × Pat ([] : List β))
+× LHS (forall (a : α) (as : List α) (b : β) (bs : List β), Pat (a::as) × Pat (b::bs))
+× LHS (forall (a : α) (as : List α), Pat (a::as) × Pat ([] : List β))
+× LHS (forall (b : β) (bs : List β), Pat ([] : List α) × Pat (b::bs))
+:= arbitrary _
+
+#eval test `ex1 2 `elimTest1
+#print elimTest1
+
+inductive Vec (α : Type u) : Nat → Type u
+| nil            : Vec 0
+| cons {n : Nat} : α → Vec n → Vec (n+1)
+
+def ex2 (α : Type u) (n : Nat) (xs : Vec α n) (ys : Vec α n) :
+  LHS (Pat (inaccessible 0) × Pat (Vec.nil : Vec α 0) × Pat (Vec.nil : Vec α 0))
+× LHS (forall (n : Nat) (x : α) (xs : Vec α n) (y : α) (ys : Vec α n), Pat (inaccessible (n+1)) × Pat (Vec.cons x xs) × Pat (Vec.cons y ys)) :=
+arbitrary _
+
+#eval test `ex2 3 `elimTest2
+#print elimTest2
+
+def ex3 (α : Type u) (β : Type v) (n : Nat) (x : List α) (y : List β) :
+  LHS (Pat ([] : List α) × Pat ([] : List β))
+× LHS (forall (a : α) (b : β), Pat [a] × Pat [b])
+× LHS (forall (a₁ a₂ : α) (as : List α) (b₁ b₂ : β) (bs : List β), Pat (a₁::a₂::as) × Pat (b₁::b₂::bs))
+× LHS (forall (as : List α) (bs : List β), Pat as × Pat bs)
+:= arbitrary _
+
+#eval test `ex3 2 `elimTest3
+#print elimTest3
+
+def ex4 (α : Type u) (n : Nat) (xs : Vec α n) :
+  LHS (Pat (inaccessible 0) × Pat (Vec.nil : Vec α 0))
+× LHS (forall (n : Nat) (xs : Vec α (n+1)), Pat (inaccessible (n+1)) × Pat xs) :=
+arbitrary _
+
+#eval test `ex4 2 `elimTest4
+#print elimTest4
+
+def ex5 (α : Type u) (n : Nat) (xs : Vec α n) :
+  LHS (Pat Nat.zero × Pat (Vec.nil : Vec α 0))
+× LHS (forall (n : Nat) (xs : Vec α (n+1)), Pat (Nat.succ n) × Pat xs) :=
+arbitrary _
+
+#eval test `ex5 2 `elimTest5
+#print elimTest5
+
+def ex6 (α : Type u) (n : Nat) (xs : Vec α n) :
+  LHS (Pat (inaccessible Nat.zero) × Pat (Vec.nil : Vec α 0))
+× LHS (forall (N : Nat) (XS : Vec α N), Pat (inaccessible N) × Pat XS) :=
+arbitrary _
+
+-- set_option trace.Meta.debug true
+
+#eval test `ex6 2 `elimTest6
+#print elimTest6
+
+def ex7 (α : Type u) (n : Nat) (xs : Vec α n) :
+  LHS (forall (a : α), Pat (inaccessible 1) × Pat (Vec.cons a Vec.nil))
+× LHS (forall (N : Nat) (XS : Vec α N), Pat (inaccessible N) × Pat XS) :=
+arbitrary _
+
+#eval test `ex7 2 `elimTest7
+#check elimTest7
+
+def isSizeOne {n : Nat} (xs : Vec Nat n) : Bool :=
+elimTest7 _ (fun _ _ => Bool) n xs (fun _ => true) (fun _ _ => false)
+
+#eval isSizeOne Vec.nil
+#eval isSizeOne (Vec.cons 1 Vec.nil)
+#eval isSizeOne (Vec.cons 2 (Vec.cons 1 Vec.nil))
+
+def singleton? {n : Nat} (xs : Vec Nat n) : Option Nat :=
+elimTest7 _ (fun _ _ => Option Nat) n xs (fun a => some a) (fun _ _ => none)
+
+#eval singleton? Vec.nil
+#eval singleton? (Vec.cons 10 Vec.nil)
+#eval singleton? (Vec.cons 20 (Vec.cons 10 Vec.nil))
+
+def ex8 (α : Type u) (n : Nat) (xs : Vec α n) :
+  LHS (forall (a b : α), Pat (inaccessible 2) × Pat (Vec.cons a (Vec.cons b Vec.nil)))
+× LHS (forall (N : Nat) (XS : Vec α N), Pat (inaccessible N) × Pat XS) :=
+arbitrary _
+
+#eval test `ex8 2 `elimTest8
+#print elimTest8
+
+def pair? {n : Nat} (xs : Vec Nat n) : Option (Nat × Nat) :=
+elimTest8 _ (fun _ _ => Option (Nat × Nat)) n xs (fun a b => some (a, b)) (fun _ _ => none)
+
+#eval pair? Vec.nil
+#eval pair? (Vec.cons 10 Vec.nil)
+#eval pair? (Vec.cons 20 (Vec.cons 10 Vec.nil))
+
+inductive Op : Nat → Nat → Type
+| mk : ∀ n, Op n n
+
+structure Node : Type :=
+(id₁ id₂ : Nat)
+(o : Op id₁ id₂)
+
+def ex9 (xs : List Node) :
+  LHS (forall (h : Node) (t : List Node), Pat (h :: Node.mk 1 1 (Op.mk 1) :: t))
+× LHS (forall (ys : List Node), Pat ys) :=
+arbitrary _
+
+#eval test `ex9 1 `elimTest9
+#print elimTest9
+
+def f (xs : List Node) : Bool :=
+elimTest9 (fun _ => Bool) xs
+  (fun _ _ => true)
+  (fun _   => false)
+
+#eval f []
+#eval f [⟨0, 0, Op.mk 0⟩]
+#eval f [⟨0, 0, Op.mk 0⟩, ⟨1, 1, Op.mk 1⟩]
+#eval f [⟨0, 0, Op.mk 0⟩, ⟨2, 2, Op.mk 2⟩]
+
+inductive Foo : Bool → Prop
+| bar : Foo false
+| baz : Foo false
+
+def ex10 (x : Bool) (y : Foo x) :
+  LHS (Pat (inaccessible false) × Pat Foo.bar)
+× LHS (forall (x : Bool) (y : Foo x), Pat (inaccessible x) × Pat y) :=
+arbitrary _
+
+#eval test `ex10 2 `elimTest10 true
+
+def ex11 (xs : List Node) :
+  LHS (forall (h : Node) (t : List Node), Pat (h :: Node.mk 1 1 (Op.mk 1) :: t))
+× LHS (Pat ([] : List Node)) :=
+arbitrary _
+
+#eval testFailure `ex11 1 `elimTest11 -- should produce error message
+
+def ex12 (x y z : Bool) :
+  LHS (forall (x y : Bool), Pat x × Pat y    × Pat true)
+× LHS (forall (x z : Bool), Pat false × Pat true × Pat z)
+× LHS (forall (y z : Bool), Pat true × Pat false × Pat z) :=
+arbitrary _
+
+#eval testFailure `ex12 3 `elimTest12 -- should produce error message
+
+def ex13 (xs : List Node) :
+  LHS (forall (h : Node) (t : List Node), Pat (h :: Node.mk 1 1 (Op.mk 1) :: t))
+× LHS (forall (ys : List Node), Pat ys)
+× LHS (forall (ys : List Node), Pat ys) :=
+arbitrary _
+
+#eval testFailure `ex13 1 `elimTest13 -- should produce error message
diff --git a/tmp/eqns/prototype.lean b/tmp/eqns/prototype.lean
deleted file mode 100644
index 93ac5c4d8d..0000000000
--- a/tmp/eqns/prototype.lean
+++ /dev/null
@@ -1,553 +0,0 @@
-import Lean.Util.CollectLevelParams
-import Lean.Meta.Check
-import Lean.Meta.Tactic.Cases
-import Lean.Meta.GeneralizeTelescope
-
-namespace Lean
-namespace Meta
-namespace DepElim
-
-inductive Pattern
-| inaccessible (ref : Syntax) (e : Expr)
-| var          (ref : Syntax) (fvarId : FVarId)
-| ctor         (ref : Syntax) (ctorName : Name) (us : List Level) (params : List Expr) (fields : List Pattern)
-| val          (ref : Syntax) (e : Expr)
-| arrayLit     (ref : Syntax) (type : Expr) (xs : List Pattern)
-
-namespace Pattern
-
-instance : Inhabited Pattern := ⟨Pattern.inaccessible Syntax.missing (arbitrary _)⟩
-
-def ref : Pattern → Syntax
-| inaccessible r _ => r
-| var r _          => r
-| ctor r _ _ _ _   => r
-| val r _          => r
-| arrayLit r _ _   => r
-
-partial def toMessageData : Pattern → MessageData
-| inaccessible _ e        => ".(" ++ e ++ ")"
-| var _ fvarId             => mkFVar fvarId
-| ctor _ ctorName _ _ []   => ctorName
-| ctor _ ctorName _ _ pats => "(" ++ ctorName ++ pats.foldl (fun (msg : MessageData) pat => msg ++ " " ++ toMessageData pat) Format.nil ++ ")"
-| val _ e                  => "val!(" ++ e ++ ")"
-| arrayLit _ _ pats        => "#[" ++ MessageData.joinSep (pats.map toMessageData) ", " ++ "]"
-
-partial def toExpr : Pattern → MetaM Expr
-| inaccessible _ e                 => pure e
-| var _ fvarId                     => pure (mkFVar fvarId)
-| val _ e                          => pure e
-| arrayLit _ type xs               => do
-  xs ← xs.mapM toExpr;
-  mkArrayLit type xs
-| ctor _ ctorName us params fields => do
-  fields ← fields.mapM toExpr;
-  pure $ mkAppN (mkConst ctorName us) (params ++ fields).toArray
-
-/- Apply the free variable substitution `s` to the given pattern -/
-partial def applyFVarSubst (s : FVarSubst) : Pattern → Pattern
-| inaccessible r e  => inaccessible r $ e.applyFVarSubst s
-| ctor r n us ps fs => ctor r n us (ps.map fun p => p.applyFVarSubst s) (fs.map applyFVarSubst)
-| val r e           => val r $ e.applyFVarSubst s
-| arrayLit r t xs   => arrayLit r (t.applyFVarSubst s) (xs.map applyFVarSubst)
-| var r fvarId      =>
-  match s.get fvarId with
-  | Expr.fvar newFVarId _ => var r newFVarId
-  | e                     => inaccessible r e
-
-def replaceFVarId (fvarId : FVarId) (e : Expr) (p : Pattern) : Pattern :=
-let s := FVarSubst.empty.insert fvarId e;
-applyFVarSubst s p
-
-end Pattern
-
-structure AltLHS :=
-(fvarDecls : List LocalDecl) -- Free variables used in the patterns.
-(patterns  : List Pattern)   -- We use `List Pattern` since we have nary match-expressions.
-
-structure Alt :=
-(idx       : Nat) -- for generating error messages
-(rhs       : Expr)
-(fvarDecls : List LocalDecl)
-(patterns  : List Pattern)
-
-namespace Alt
-
-instance : Inhabited Alt := ⟨⟨0, arbitrary _, [], []⟩⟩
-
-partial def toMessageData (alt : Alt) : MetaM MessageData := do
-lctx ← getLCtx;
-localInsts ← getLocalInstances;
-let lctx := alt.fvarDecls.foldl (fun (lctx : LocalContext) decl => lctx.addDecl decl) lctx;
-withLocalContext lctx localInsts do
-  let msg : MessageData := "⟦" ++ MessageData.joinSep (alt.patterns.map Pattern.toMessageData) ", " ++ "⟧ := " ++ alt.rhs;
-  addContext msg
-
-def applyFVarSubst (s : FVarSubst) (alt : Alt) : Alt :=
-{ alt with
-  patterns  := alt.patterns.map fun p => p.applyFVarSubst s,
-  fvarDecls := alt.fvarDecls.map fun d => d.applyFVarSubst s,
-  rhs       := alt.rhs.applyFVarSubst s }
-
-end Alt
-
-structure Problem :=
-(goal          : Expr)
-(vars          : List Expr)
-(alts          : List Alt)
-
-def withGoalOf {α} (p : Problem) (x : MetaM α) : MetaM α :=
-withMVarContext p.goal.mvarId! x
-
-namespace Problem
-
-instance : Inhabited Problem := ⟨{ goal := arbitrary _, vars := [], alts := []}⟩
-
-def toMessageData (p : Problem) : MetaM MessageData :=
-withGoalOf p do
-  alts ← p.alts.mapM Alt.toMessageData;
-  pure $ "vars " ++ p.vars.toArray
-    -- ++ Format.line ++ "var ids " ++ toString (p.vars.map (fun x => match x with | Expr.fvar id _ => toString id | _ => "[nonvar]"))
-    ++ Format.line ++ MessageData.joinSep alts Format.line
-
-end Problem
-
-structure ElimResult :=
-(elim      : Expr) -- The eliminator. It is not just `Expr.const elimName` because the type of the major premises may contain free variables.
-
-/- The number of patterns in each AltLHS must be equal to majors.length -/
-private def checkNumPatterns (majors : List Expr) (lhss : List AltLHS) : MetaM Unit :=
-let num := majors.length;
-when (lhss.any (fun lhs => lhs.patterns.length != num)) $
-  throw $ Exception.other "incorrect number of patterns"
-
-/-
- Given major premises `(x_1 : A_1) (x_2 : A_2[x_1]) ... (x_n : A_n[x_1, x_2, ...])`, return
- `forall (x_1 : A_1) (x_2 : A_2[x_1]) ... (x_n : A_n[x_1, x_2, ...]), sortv` -/
-private def withMotive {α} (majors : Array Expr) (sortv : Expr) (k : Expr → MetaM α) : MetaM α := do
-type ← mkForall majors sortv;
-trace! `Meta.debug ("motive: " ++ type);
-withLocalDecl `motive type BinderInfo.default k
-
-private partial def withAltsAux {α} (motive : Expr) : List AltLHS → List Alt → Array Expr → (List Alt → Array Expr → MetaM α) → MetaM α
-| [],        alts, minors, k => k alts.reverse minors
-| lhs::lhss, alts, minors, k => do
-  let xs := lhs.fvarDecls.toArray.map LocalDecl.toExpr;
-  minorType ← withExistingLocalDecls lhs.fvarDecls do {
-    args ← lhs.patterns.toArray.mapM Pattern.toExpr;
-    let minorType := mkAppN motive args;
-    mkForall xs minorType
-  };
-  let idx       := alts.length;
-  let minorName := (`h).appendIndexAfter (idx+1);
-  trace! `Meta.debug ("minor premise " ++ minorName ++ " : " ++ minorType);
-  withLocalDecl minorName minorType BinderInfo.default fun minor =>
-    let rhs    := mkAppN minor xs;
-    let minors := minors.push minor;
-    let alts   := { idx := idx, rhs := rhs, fvarDecls := lhs.fvarDecls, patterns := lhs.patterns : Alt } :: alts;
-    withAltsAux lhss alts minors k
-
-/- Given a list of `AltLHS`, create a minor premise for each one, convert them into `Alt`, and then execute `k` -/
-private partial def withAlts {α} (motive : Expr) (lhss : List AltLHS) (k : List Alt → Array Expr → MetaM α) : MetaM α :=
-withAltsAux motive lhss [] #[] k
-
-def assignGoalOf (p : Problem) (e : Expr) : MetaM Unit :=
-withGoalOf p (assignExprMVar p.goal.mvarId! e)
-
-structure State :=
-(used   : Std.HashSet Nat := {}) -- used alternatives
-
-/-- Return true if the given (sub-)problem has been solved. -/
-private def isDone (p : Problem) : Bool :=
-p.vars.isEmpty
-
-private def isAltDecl (alt : Alt) (fvarId : FVarId) : Bool :=
-alt.fvarDecls.any fun d => d.fvarId == fvarId
-
-/- Return true if the next pattern of each remaining alternative is an inaccessible term or a variable -/
-private def isVariableTransition (p : Problem) : Bool :=
-p.alts.all fun alt => match alt.patterns with
-  | Pattern.inaccessible _ _ :: _ => true
-  | Pattern.var _ _ :: _          => true
-  | _                             => false
-
-/- Return true if the next pattern of each remaining alternative is a constructor application -/
-private def isConstructorTransition (p : Problem) : Bool :=
-p.alts.all fun alt => match alt.patterns with
-  | Pattern.ctor _ _ _ _ _ :: _ => true
-  | _                           => false
-
-/- Return true if the next pattern of the remaining alternatives contain variables AND constructors. -/
-private def isCompleteTransition (p : Problem) : Bool :=
-let (ok, hasVar, hasCtor) := p.alts.foldl
-  (fun (acc : Bool × Bool × Bool) (alt : Alt) =>
-    let (ok, hasVar, hasCtor) := acc;
-    match alt.patterns with
-    | Pattern.ctor _ _ _ _ _ :: _ => (ok, hasVar, true)
-    | Pattern.var _ fvarId :: _   => if isAltDecl alt fvarId then (ok, true, hasCtor) else (false, hasVar, hasCtor)
-    | _                           => (false, hasVar, hasCtor))
-  (true, false, false);
-ok && hasVar && hasCtor
-
-private def processLeaf (p : Problem) (s : State) : MetaM State := do
-let alt := p.alts.head!;
-assignGoalOf p alt.rhs;
-pure { s with used := s.used.insert alt.idx }
-
-private def replaceFVarIdAtLocalDecl (fvarId : FVarId) (e : Expr) (d : LocalDecl) : LocalDecl :=
-if d.fvarId == fvarId then d
-else match d with
-  | LocalDecl.cdecl idx id n type bi  => LocalDecl.cdecl idx id n (type.replaceFVarId fvarId e) bi
-  | LocalDecl.ldecl idx id n type val => LocalDecl.ldecl idx id n (type.replaceFVarId fvarId e) (val.replaceFVarId fvarId e)
-
-private def processVariable (process : Problem → State → MetaM State) (p : Problem) (s : State) : MetaM State := do
-match p.vars with
-| x :: xs =>
-  let alts := p.alts.map fun alt => match alt.patterns with
-    | Pattern.inaccessible _ _ :: ps => { alt with patterns := ps }
-    | Pattern.var _ fvarId :: ps     =>
-      if isAltDecl alt fvarId then
-        let patterns  := ps.map (fun p => p.replaceFVarId fvarId x);
-        let rhs       := alt.rhs.replaceFVarId fvarId x;
-        /- We eliminate the LocalDecl for fvarId since it was substituted. -/
-        let fvarDecls := alt.fvarDecls.filter fun d => d.fvarId != fvarId;
-        let fvarDecls := fvarDecls.map $ replaceFVarIdAtLocalDecl fvarId x;
-        { alt with patterns := patterns, rhs := rhs, fvarDecls := fvarDecls }
-      else
-        { alt with patterns := ps }
-    | _                              => unreachable!;
-  process { p with alts := alts, vars := xs } s
-| _ => unreachable!
-
-private def isFirstPatternCtor (ctorName : Name) (alt : Alt) : Bool :=
-match alt.patterns with
-| Pattern.ctor _ n _ _ _ :: _ => n == ctorName
-| _                           => false
-
-private def expandCtorPattern (alt : Alt) : Alt :=
-match alt.patterns with
-| Pattern.ctor _ _ _ _ fields :: ps => { alt with patterns := fields ++ ps }
-| _                                 => alt
-
-private def processConstructor (process : Problem → State → MetaM State) (p : Problem) (s : State) : MetaM State :=
-match p.vars with
-| x :: xs => do
-  subgoals ← cases p.goal.mvarId! x.fvarId!;
-  subgoals.foldlM
-    (fun (s : State) subgoal =>
-      let newVars := subgoal.fields.toList.map mkFVar ++ xs;
-      let newVars := newVars.map fun x => x.applyFVarSubst subgoal.subst;
-      let newAlts := p.alts.filter $ isFirstPatternCtor subgoal.ctorName;
-      let newAlts := newAlts.map fun alt => match alt.patterns with
-        | Pattern.ctor _ _ _ _ fields :: ps => { alt with patterns := fields ++ ps }
-        | _                                 => unreachable!;
-      let newAlts := newAlts.map fun alt => alt.applyFVarSubst subgoal.subst;
-      process { goal := mkMVar subgoal.mvarId, vars := newVars, alts := newAlts } s)
-    s
-| _ => unreachable!
-
-private def throwInductiveTypeExpected {α} (e : Expr) : MetaM α := do
-t ← inferType e;
-throwOther ("failed to compile pattern matching, inductive type expected" ++ indentExpr e ++ Format.line ++ "has type" ++ indentExpr t)
-
-/- Auxiliary method for `processComplete` -/
-private partial def mkCompatibleCtorPattern (ref : Syntax) (ctorName : Name) (us : List Level) (params : Array Expr)
-    (mvars : Array Expr) (varNamePrefix : Name) : Nat → Array LocalDecl → Array Pattern → MetaM (List LocalDecl × Pattern)
-| i, newDecls, fields =>
-  if h : i < mvars.size then do
-    let mvar := mvars.get ⟨i, h⟩;
-    e ← instantiateMVars mvar;
-    match e with
-    | Expr.mvar _ _ => do
-      type ← inferType e;
-      withLocalDecl (varNamePrefix.appendIndexAfter i) type BinderInfo.default fun x => do
-        decl ← getLocalDecl x.fvarId!;
-        mkCompatibleCtorPattern (i+1) (newDecls.push decl) (fields.push (Pattern.var ref decl.fvarId))
-    | Expr.fvar fvarId _ => mkCompatibleCtorPattern (i+1) newDecls (fields.push (Pattern.var ref fvarId))
-    | _ => mkCompatibleCtorPattern (i+1) newDecls (fields.push (Pattern.inaccessible ref e))
-  else
-    pure (newDecls.toList, Pattern.ctor ref ctorName us params.toList fields.toList)
-
-/- Auxiliary method for `processComplete` -/
-private partial def compatibleConstructor? (ref : Syntax) (ctorName : Name) (us : List Level) (params : Array Expr) (expectedType : Expr)
-    (varNamePrefix : Name) : MetaM (Option (List LocalDecl × Pattern)) := do
-let ctor := mkAppN (mkConst ctorName us) params;
-ctorType ← inferType ctor;
-(mvars, _, resultType) ← forallMetaTelescopeReducing ctorType;
-trace! `Meta.debug ("ctorName: " ++ ctorName ++ ", resultType: " ++ resultType ++ ", expectedType: " ++ expectedType);
-condM (isDefEq resultType expectedType)
-  (Option.some <$> mkCompatibleCtorPattern ref ctorName us params mvars varNamePrefix 0 #[] #[])
-  (pure none)
-
-/- Auxiliary method for `processComplete` -/
-private def getCompatibleConstructors (ref : Syntax) (e : Expr) (varNamePrefix : Name) : MetaM (List (List LocalDecl × Pattern)) := do
-env ← getEnv;
-expectedType ← inferType e;
-expectedType ← whnfD expectedType;
-let I     := expectedType.getAppFn;
-let Iargs := expectedType.getAppArgs;
-matchConst env I (fun _ => throwInductiveTypeExpected e) fun info us =>
-match info with
-| ConstantInfo.inductInfo val =>
-  let params := Iargs.extract 0 val.nparams;
-  val.ctors.foldlM
-    (fun (result : List (List LocalDecl × Pattern)) ctor => do
-      entry? ← withNewMCtxDepth $ compatibleConstructor? ref ctor us params expectedType varNamePrefix;
-      match entry? with
-      | none       => pure result
-      | some entry => pure (entry :: result))
-    []
-| _ => throwInductiveTypeExpected e
-
-/- Auxiliary method for `processComplete` -/
-private def processComplete (process : Problem → State → MetaM State) (p : Problem) (s : State) : MetaM State :=
-withGoalOf p do
-env ← getEnv;
-newAlts ← p.alts.foldlM
-  (fun (newAlts : List Alt) alt =>
-    match alt.patterns with
-    | Pattern.ctor _ _ _ _ _ :: ps => pure (alt :: newAlts)
-    | p@(Pattern.var ref fvarId) :: ps =>
-      withExistingLocalDecls alt.fvarDecls do
-        ldecl ← getLocalDecl fvarId;
-        dps ← getCompatibleConstructors p.ref (mkFVar fvarId) ldecl.userName;
-        expandedAlts ← dps.mapM fun ⟨newLocalDecls, p⟩ => do {
-          e ← p.toExpr;
-          let ps  := ps.map fun p => p.replaceFVarId fvarId e;
-          let rhs := alt.rhs.replaceFVarId fvarId e;
-          let fvarDecls := alt.fvarDecls.map (replaceFVarIdAtLocalDecl fvarId e);
-          pure { alt with patterns := p :: ps, fvarDecls := fvarDecls ++ newLocalDecls, rhs := rhs }
-        };
-        pure (expandedAlts ++ newAlts)
-    | _ => unreachable!)
-  [];
-process { p with alts := newAlts.reverse } s
-
-private partial def process : Problem → State → MetaM State
-| p, s => withIncRecDepth do
-  withGoalOf p (traceM `Meta.debug p.toMessageData);
-  if isDone p then
-    processLeaf p s
-  else if isVariableTransition p then
-    processVariable process p s
-  else if isConstructorTransition p then
-    processConstructor process p s
-  else if isCompleteTransition p then
-    processComplete process p s
-  else do
-    msg ← p.toMessageData;
-    -- TODO: remaining cases
-    throwOther ("not implement yet " ++ msg)
-
-def getUnusedLevelParam (majors : List Expr) (lhss : List AltLHS) : MetaM Level := do
-let s : CollectLevelParams.State := {};
-s ← majors.foldlM
-  (fun s major => do
-    major ← instantiateMVars major;
-    majorType ← inferType major;
-    majorType ← instantiateMVars majorType;
-    let s := collectLevelParams s major;
-    pure $ collectLevelParams s majorType)
-  s;
-pure s.getUnusedLevelParam
-
-/- Return `Prop` if `inProf == true` and `Sort u` otherwise, where `u` is a fresh universe level parameter. -/
-private def mkElimSort (majors : List Expr) (lhss : List AltLHS) (inProp : Bool) : MetaM Expr :=
-if inProp then
-  pure $ mkSort $ levelZero
-else do
-  v ← getUnusedLevelParam majors lhss;
-  pure $ mkSort $ v
-
-def mkElim (elimName : Name) (majors : List Expr) (lhss : List AltLHS) (inProp : Bool := false) : MetaM ElimResult := do
-checkNumPatterns majors lhss;
-sortv ← mkElimSort majors lhss inProp;
-generalizeTelescope majors.toArray `_d fun majors => do
-withMotive majors sortv fun motive => do
-let target  := mkAppN motive majors;
-trace! `Meta.debug ("target: " ++ target);
-withAlts motive lhss fun alts minors => do
-  goal ← mkFreshExprMVar target;
-  s    ← process { goal := goal, vars := majors.toList, alts := alts } {};
-  let args := #[motive] ++ majors ++ minors;
-  type ← mkForall args target;
-  val  ← mkLambda args goal;
-  trace! `Meta.debug ("eliminator value: " ++ val ++ "\ntype: " ++ type);
-  elim ← mkAuxDefinition elimName type val;
-  trace! `Meta.debug ("eliminator: " ++ elim);
-  pure { elim := elim }
-
-end DepElim
-end Meta
-end Lean
-
-open Lean
-open Lean.Meta
-open Lean.Meta.DepElim
-
-/- Infrastructure for testing -/
-
-universes u v
-
-def inaccessible {α : Sort u} (a : α) : α := a
-def val {α : Sort u} (a : α) : α := a
-
-private def getConstructorVal (ctorName : Name) (fn : Expr) (args : Array Expr) : MetaM (Option (ConstructorVal × Expr × Array Expr)) := do
-env ← getEnv;
-match env.find? ctorName with
-| some (ConstantInfo.ctorInfo v) => if args.size == v.nparams + v.nfields then pure $ some (v, fn, args) else pure none
-| _                              => pure none
-
-private def constructorApp? (e : Expr) : MetaM (Option (ConstructorVal × Expr × Array Expr)) := do
-env ← getEnv;
-match e with
-| Expr.lit (Literal.natVal n) _ =>
-   if n == 0 then getConstructorVal `Nat.zero (mkConst `Nat.zero) #[] else getConstructorVal `Nat.succ (mkConst `Nat.succ) #[mkNatLit (n-1)]
-| _ =>
-  let fn := e.getAppFn;
-  match fn with
-  | Expr.const n _ _ => getConstructorVal n fn e.getAppArgs
-  | _                => pure none
-
-/- Convert expression using auxiliary hints `inaccessible` and `val` into a pattern -/
-partial def mkPattern : Expr → MetaM Pattern
-| e =>
-  if e.isAppOfArity `val 2 then
-    pure $ Pattern.val Syntax.missing e.appArg!
-  else if e.isAppOfArity `inaccessible 2 then
-    pure $ Pattern.inaccessible Syntax.missing e.appArg!
-  else if e.isFVar then
-    pure $ Pattern.var Syntax.missing e.fvarId!
-  else match e.arrayLit? with
-    | some es => do
-      pats ← es.mapM mkPattern;
-      type ← inferType e;
-      type ← whnfD type;
-      let elemType := type.appArg!;
-      pure $ Pattern.arrayLit Syntax.missing elemType pats
-    | none => do
-      r? ← constructorApp? e;
-      match r? with
-      | none      => throw $ Exception.other "unexpected pattern"
-      | some (cval, fn, args) => do
-        let params := args.extract 0 cval.nparams;
-        let fields := args.extract cval.nparams args.size;
-        pats ← fields.toList.mapM mkPattern;
-        pure $ Pattern.ctor Syntax.missing cval.name fn.constLevels! params.toList pats
-
-partial def decodePats : Expr → MetaM (List Pattern)
-| e =>
-  match e.app2? `Pat with
-  | some (_, pat) => do pat ← mkPattern pat; pure [pat]
-  | none =>
-    match e.prod? with
-    | none => throw $ Exception.other "unexpected pattern"
-    | some (pat, pats) => do
-      pat  ← decodePats pat;
-      pats ← decodePats pats;
-      pure (pat ++ pats)
-
-partial def decodeAltLHS (e : Expr) : MetaM AltLHS :=
-forallTelescopeReducing e fun args body => do
-  decls ← args.toList.mapM (fun arg => getLocalDecl arg.fvarId!);
-  pats  ← decodePats body;
-  pure { fvarDecls := decls, patterns := pats }
-
-partial def decodeAltLHSs : Expr → MetaM (List AltLHS)
-| e =>
-  match e.app2? `LHS with
-  | some (_, lhs) => do lhs ← decodeAltLHS lhs; pure [lhs]
-  | none =>
-    match e.prod? with
-    | none => throw $ Exception.other "unexpected LHS"
-    | some (lhs, lhss) => do
-      lhs  ← decodeAltLHSs lhs;
-      lhss ← decodeAltLHSs lhss;
-      pure (lhs ++ lhss)
-
-def withDepElimFrom {α} (declName : Name) (numPats : Nat) (k : List FVarId → List AltLHS → MetaM α) : MetaM α := do
-cinfo ← getConstInfo declName;
-forallTelescopeReducing cinfo.type fun args body =>
-  if args.size < numPats then
-    throw $ Exception.other "insufficient number of parameters"
-  else do
-    let xs := (args.extract (args.size - numPats) args.size).toList.map $ Expr.fvarId!;
-    alts ← decodeAltLHSs body;
-    k xs alts
-
-inductive Pat {α : Sort u} (a : α) : Type u
-| mk : Pat
-
-inductive LHS {α : Sort u} (a : α) : Type u
-| mk : LHS
-
-instance LHS.inhabited {α} (a : α) : Inhabited (LHS a) := ⟨LHS.mk⟩
-
--- set_option trace.Meta.debug true
--- set_option trace.Meta.Tactic.cases true
--- set_option trace.Meta.Tactic.subst true
-
-@[init] def register : IO Unit :=
-registerTraceClass `Meta.mkElim
-
-def test (ex : Name) (numPats : Nat) (elimName : Name) : MetaM Unit :=
-withDepElimFrom ex numPats fun majors alts => do
-  let majors := majors.map mkFVar;
-  trace! `Meta.debug ("majors: " ++ majors.toArray);
-  _ ← mkElim elimName majors alts;
-  pure ()
-
-def ex0 (x : Nat) : LHS (forall (y : Nat), Pat y)
-:= arbitrary _
-
-#eval test `ex0 1 `elimTest0
-#print elimTest0
-
-def ex1 (α : Type u) (β : Type v) (n : Nat) (x : List α) (y : List β) :
-  LHS (Pat ([] : List α) × Pat ([] : List β))
-× LHS (forall (a : α) (as : List α) (b : β) (bs : List β), Pat (a::as) × Pat (b::bs))
-× LHS (forall (a : α) (as : List α), Pat (a::as) × Pat ([] : List β))
-× LHS (forall (b : β) (bs : List β), Pat ([] : List α) × Pat (b::bs))
-:= arbitrary _
-
-#eval test `ex1 2 `elimTest1
-#print elimTest1
-
-inductive Vec (α : Type u) : Nat → Type u
-| nil            : Vec 0
-| cons {n : Nat} : α → Vec n → Vec (n+1)
-
-def ex2 (α : Type u) (n : Nat) (xs : Vec α n) (ys : Vec α n) :
-  LHS (Pat (inaccessible 0) × Pat (Vec.nil : Vec α 0) × Pat (Vec.nil : Vec α 0))
-× LHS (forall (n : Nat) (x : α) (xs : Vec α n) (y : α) (ys : Vec α n), Pat (inaccessible (n+1)) × Pat (Vec.cons x xs) × Pat (Vec.cons y ys)) :=
-arbitrary _
-
-#eval test `ex2 3 `elimTest2
-#print elimTest2
-
-def ex3 (α : Type u) (β : Type v) (n : Nat) (x : List α) (y : List β) :
-  LHS (Pat ([] : List α) × Pat ([] : List β))
-× LHS (forall (a : α) (b : β), Pat [a] × Pat [b])
-× LHS (forall (a₁ a₂ : α) (as : List α) (b₁ b₂ : β) (bs : List β), Pat (a₁::a₂::as) × Pat (b₁::b₂::bs))
-× LHS (forall (as : List α) (bs : List β), Pat as × Pat bs)
-:= arbitrary _
-
-#eval test `ex3 2 `elimTest3
-#print elimTest3
-
-def ex4 (α : Type u) (n : Nat) (xs : Vec α n) :
-  LHS (Pat (inaccessible 0) × Pat (Vec.nil : Vec α 0))
-× LHS (forall (n : Nat) (xs : Vec α (n+1)), Pat (inaccessible (n+1)) × Pat xs) :=
-arbitrary _
-
-#eval test `ex4 2 `elimTest4
-#check elimTest4
-#print elimTest4
-
-def ex5 (α : Type u) (n : Nat) (xs : Vec α n) :
-  LHS (Pat Nat.zero × Pat (Vec.nil : Vec α 0))
-× LHS (forall (n : Nat) (xs : Vec α (n+1)), Pat (Nat.succ n) × Pat xs) :=
-arbitrary _
-
-#eval test `ex5 2 `elimTest5
-#print elimTest5