Merge branch 'dev' into serial/env-extensions

Pantograph/Delate.lean

@@ -63,7 +63,10 @@ def exprProjToApp (env : Environment) (e : Expr) : Expr :=
       (List.range numFields)
     mkAppN callee (typeArgs ++ [motive, major, induct]).toArray
 
-def _root_.Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _
+def _root_.Lean.Name.isAuxLemma (n : Name) : Bool :=
+  match n with
+  | .str _ s => "_proof_".isPrefixOf s
+  | _ => false
 
 /-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/
 @[export pantograph_unfold_aux_lemmas_m]

Test/Environment.lean

@@ -30,7 +30,6 @@ def test_symbol_visibility: IO LSpec.TestSeq := do
   let entries: List (Name × Bool) := [
     ("Nat.add_comm".toName, false),
     ("foo.bla.Init.Data.List.Basic.2.1.Init.Lean.Expr._hyg.4".toName, true),
-    ("Init.Data.Nat.Basic._auxLemma.4".toName, true),
   ]
   let suite := entries.foldl (λ suites (symbol, target) =>
     let test := LSpec.check symbol.toString ((Environment.isNameInternal symbol) == target)

Test/Metavar.lean

@@ -162,7 +162,7 @@ def test_m_couple_simp: TestM Unit := do
   checkEq "(5 root)" rootStr "Nat.le_trans (of_eq_true (_proof_4✝ 2)) (of_eq_true (eq_true_of_decide (Eq.refl true)))"
   let unfoldedRoot ←  unfoldAuxLemmas root
   checkEq "(5 root)" (toString (← Lean.Meta.ppExpr unfoldedRoot))
-    "Nat.le_trans (of_eq_true (_proof_4✝ 2)) (of_eq_true (eq_true_of_decide (Eq.refl true)))"
+    "Nat.le_trans (of_eq_true (eq_true (Nat.le_refl 2))) (of_eq_true (eq_true_of_decide (Eq.refl true)))"
   return ()
 
 def test_proposition_generation: TestM Unit := do