chore: fix tests

tests/lean/abst.lean

@@ -5,8 +5,8 @@ open Lean
 def tst : IO Unit :=
 do
 let f := mkConst `f;
-let x := mkFVar `x;
-let y := mkFVar `y;
+let x := mkFVar { name := `x };
+let y := mkFVar { name := `y };
 let t := mkApp (mkApp (mkApp f x) y) (mkApp f x);
 IO.println t;
 let p := t.abstract [x, y].toArray;

tests/lean/mvar1.lean

@@ -22,6 +22,12 @@ def natE  := mkConst `Nat []
 def boolE := mkConst `Bool []
 def vecE  := mkConst `Vec [levelZero]
 
+instance : Coe Name FVarId where
+  coe n := { name := n }
+
+instance : Coe Name MVarId where
+  coe n := { name := n }
+
 def α := mkFVar `α
 def x := mkFVar `x
 def y := mkFVar `y

tests/lean/mvar2.lean

@@ -22,6 +22,12 @@ def natE  := mkConst `Nat []
 def boolE := mkConst `Bool []
 def vecE  := mkConst `Vec [levelZero]
 
+instance : Coe Name FVarId where
+  coe n := { name := n }
+
+instance : Coe Name MVarId where
+  coe n := { name := n }
+
 def α := mkFVar `α
 def x := mkFVar `x
 def y := mkFVar `y

tests/lean/mvar3.lean

@@ -28,6 +28,12 @@ def natE  := mkConst `Nat
 def boolE := mkConst `Bool
 def vecE  := mkConst `Vec [levelZero]
 
+instance : Coe Name FVarId where
+  coe n := { name := n }
+
+instance : Coe Name MVarId where
+  coe n := { name := n }
+
 def α := mkFVar `α
 def x := mkFVar `x
 def y := mkFVar `y
@@ -62,10 +68,13 @@ def mctx5 := R1.1
 def sortNames (xs : List Name) : List Name :=
 (xs.toArray.qsort Name.lt).toList
 
-def sortNamePairs {α} [Inhabited α] (xs : List (Name × α)) : List (Name × α) :=
-(xs.toArray.qsort (fun a b => Name.lt a.1 b.1)).toList
+instance : ToString MVarId where
+  toString m := toString m.name
 
-#eval toString $ sortNames $ mctx5.decls.toList.map Prod.fst
+def sortNamePairs {α} [Inhabited α] (xs : List (MVarId × α)) : List (MVarId × α) :=
+(xs.toArray.qsort (fun a b => Name.lt a.1.name b.1.name)).toList
+
+#eval toString $ sortNames $ mctx5.decls.toList.map (·.1.name)
 #eval toString $ sortNamePairs $ mctx5.eAssignment.toList
 #eval e1
 #eval check (!e1.hasFVar)
@@ -77,10 +86,10 @@ match mkLambdaTest mctx4' {namePrefix := `n} lctx4 #[α, x, y] $ mkAppN f #[m3,
 def e2    := R2.2.2
 def mctx6 := R2.1
 
-#eval toString $ sortNames $ mctx6.decls.toList.map Prod.fst
+#eval toString $ sortNames $ mctx6.decls.toList.map (·.1.name)
 #eval toString $ sortNamePairs $ mctx6.eAssignment.toList
 -- ?n.2 was delayed assigned because ?m.3 is synthetic
-#eval toString $ sortNames $ mctx6.dAssignment.toList.map Prod.fst
+#eval toString $ sortNames $ mctx6.dAssignment.toList.map (·.1.name)
 #eval e2
 
 #print "assigning ?m1 and ?n.1"

tests/lean/mvar_fvar.lean

@@ -2,6 +2,12 @@ import Lean
 
 open Lean
 
+instance : Coe Name FVarId where
+  coe n := { name := n }
+
+instance : Coe Name MVarId where
+  coe n := { name := n }
+
 #eval (mkFVar `a).hasFVar
 #eval (mkApp (mkConst `foo) (mkFVar `a)).hasFVar
 #eval (mkApp (mkConst `foo) (mkConst `a)).hasFVar

tests/lean/run/closure1.lean

@@ -15,6 +15,12 @@ def printDef (declName : Name) : MetaM Unit := do
 let cinfo ← getConstInfo declName;
 trace[Meta.debug] cinfo.value!
 
+instance : Coe Name FVarId where
+  coe n := { name := n }
+
+instance : Coe Name MVarId where
+  coe n := { name := n }
+
 def tst1 : MetaM Unit := do
 let u := mkLevelParam `u
 let v := mkLevelMVar  `v

tests/lean/run/expr1.lean

@@ -108,6 +108,8 @@ pure ()
 
 #eval tst6
 
+instance : Coe Name FVarId where
+  coe n := { name := n }
 
 def tst7 : IO Unit := do
 let x := mkFVar `x;

tests/lean/run/meta5.lean

@@ -16,7 +16,7 @@ withLetDecl `x (mkConst `Nat) (mkNatLit 0) $ fun x => do {
   trace[Meta.debug] r;
   let mctx ← getMCtx;
   mctx.decls.forM fun mvarId mvarDecl => do
-    trace[Meta.debug] m!"?{mvarId} : {mvarDecl.type}"
+    trace[Meta.debug] m!"?{mvarId.name} : {mvarDecl.type}"
 }
 
 set_option trace.Meta.debug true