From 7d9d3e47421aa59aa3d993d41b5b4c81df2cdf35 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 19 Jun 2025 15:47:16 -0700 Subject: [PATCH] fix: Use the correct unfold aux lemma --- Pantograph/Delate.lean | 5 ++++- Test/Environment.lean | 1 - Test/Metavar.lean | 2 +- 3 files changed, 5 insertions(+), 3 deletions(-) diff --git a/Pantograph/Delate.lean b/Pantograph/Delate.lean index a021b72..3dae649 100644 --- a/Pantograph/Delate.lean +++ b/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] diff --git a/Test/Environment.lean b/Test/Environment.lean index 13afbfd..354473e 100644 --- a/Test/Environment.lean +++ b/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) diff --git a/Test/Metavar.lean b/Test/Metavar.lean index a3b03eb..ddd6e56 100644 --- a/Test/Metavar.lean +++ b/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 -- 2.44.1