From 53a7957b8e1955c1b307ffca31bf10c1b366c3fa Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 29 Jul 2020 14:32:07 -0700
Subject: [PATCH] chore: fix prototype

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

diff --git a/tmp/eqns/prototype.lean b/tmp/eqns/prototype.lean
index 0a8096328e..31dce8e889 100644
--- a/tmp/eqns/prototype.lean
+++ b/tmp/eqns/prototype.lean
@@ -1,7 +1,6 @@
-prelude
-import Init.Lean.Meta.Check
-import Init.Lean.Meta.Tactic.Cases
-import Init.Lean.Meta.GeneralizeTelescope
+import Lean.Meta.Check
+import Lean.Meta.Tactic.Cases
+import Lean.Meta.GeneralizeTelescope
 
 namespace Lean
 namespace Meta
@@ -36,7 +35,7 @@ structure MinorsRange :=
 (firstMinorPos : Nat)
 (numMinors     : Nat)
 
-abbrev AltToMinorsMap := PersistentHashMap Nat MinorsRange
+abbrev AltToMinorsMap := Std.PersistentHashMap Nat MinorsRange
 
 structure Alt :=
 (idx       : Nat) -- for generating error messages
@@ -114,7 +113,7 @@ withMotive majors sortv $ fun motive => do
 let target  := mkAppN motive majors;
 goal ← mkFreshExprMVar target;
 let alts    := mkAlts lhss;
-let problem := { Problem . goal := goal, vars := majors.toList, alts := alts };
+let problem := { goal := goal, vars := majors.toList, alts := alts : Problem };
 process problem;
 pure { numMinors := 0, numEqs := 0, elim := arbitrary _, altMap := {} } -- TODO
 
@@ -197,10 +196,10 @@ forallTelescopeReducing cinfo.type $ fun args body =>
     k xs alts
 
 inductive Pat {α : Sort u} (a : α) : Type u
-| mk {} : Pat
+| mk : Pat
 
 inductive LHS {α : Sort u} (a : α) : Type u
-| mk {} : LHS
+| mk : LHS
 
 instance LHS.inhabited {α} (a : α) : Inhabited (LHS a) := ⟨LHS.mk⟩
 
@@ -220,7 +219,7 @@ def tst1 : MetaM Unit :=
 withDepElimFrom `ex1 2 $ fun majors alts => do
   let majors := majors.map mkFVar;
   trace! `Meta.debug majors.toArray;
-  mkElim `test majors alts;
+  _ ← mkElim `test majors alts;
   pure ()
 
 #eval tst1