From fdfa3fc0de415fc974d6c4e3657445760e0dcba8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 19 Mar 2020 17:01:59 -0700
Subject: [PATCH] chore: minor

---
 tmp/eqns/prototype.lean | 17 ++++++++++++-----
 1 file changed, 12 insertions(+), 5 deletions(-)

diff --git a/tmp/eqns/prototype.lean b/tmp/eqns/prototype.lean
index d2aa0c7c05..292df10467 100644
--- a/tmp/eqns/prototype.lean
+++ b/tmp/eqns/prototype.lean
@@ -56,8 +56,14 @@ structure ElimResult :=
 (elim      : Expr) -- The eliminator. It is not just `Expr.const elimName` because the type of the major premises may contain free variables.
 (altMap    : AltToMinorsMap) -- each alternative may be "expanded" into multiple minor premise
 
-def mkElim (elimName : Name) (xs : List FVarId) (lhss : List AltLHS) : MetaM ElimResult :=
-throw $ arbitrary _
+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"
+
+def mkElim (elimName : Name) (majors : List Expr) (lhss : List AltLHS) : MetaM ElimResult := do
+checkNumPatterns majors lhss;
+pure { numMinors := 0, numEqs := 0, elim := arbitrary _, altMap := {} } -- TODO
 
 end DepElim
 end Meta
@@ -131,13 +137,13 @@ partial def decodeAltLHSs : Expr → MetaM (List AltLHS)
       lhss ← decodeAltLHSs lhss;
       pure (lhs ++ lhss)
 
-def mkDepElimFrom (declName : Name) (numPats : Nat) : MetaM (List FVarId × List AltLHS) := do
+def mkDepElimFrom (declName : Name) (numPats : Nat) : MetaM (List Expr × List AltLHS) := 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!;
+    let xs := (args.extract (args.size - numPats) args.size).toList;
     alts ← decodeAltLHSs body;
     pure (xs, alts)
 
@@ -159,8 +165,9 @@ def ex1 (α : Type u) (β : Type v) (n : Nat) (x : List α) (y : List β) :
 set_option trace.Meta.debug true
 
 def tst1 : MetaM Unit := do
-(xs, alts) ← mkDepElimFrom `ex1 2;
+(majors, alts) ← mkDepElimFrom `ex1 2;
 printAltLHS alts;
+mkElim `test majors alts;
 pure ()
 
 #eval tst1