aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 15 Pull Requests 3 Packages Projects Releases Wiki Activity

Merge pull request 'fix: Use the correct unfold aux lemma' (#215) from bug/unfold-aux-lemma into dev 

Reviewed-on: #215
This commit is contained in:
Leni Aniva 2025-06-20 10:21:00 -07:00
parent 9a8b5040f5 7d9d3e4742
commit 0db2451c8a
3 changed files with 5 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
Pantograph/Delate.lean
View File

@ -63,7 +63,10 @@ def exprProjToApp (env : Environment) (e : Expr) : Expr :=
(List.range numFields) (List.range numFields)
mkAppN callee (typeArgs ++ [motive, major, induct]).toArray 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. -/ /-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/
@[export pantograph_unfold_aux_lemmas_m] @[export pantograph_unfold_aux_lemmas_m]

1
Test/Environment.lean
View File

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

2
Test/Metavar.lean
View File

@ -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)))" 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 let unfoldedRoot ← unfoldAuxLemmas root
checkEq "(5 root)" (toString (← Lean.Meta.ppExpr unfoldedRoot)) 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 () return ()
def test_proposition_generation: TestM Unit := do def test_proposition_generation: TestM Unit := do