From d035efbb874f24924629d60057af8f8fc61bb974 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Wojciech=20R=C3=B3=C5=BCowski?= Date: Thu, 19 Feb 2026 15:17:55 +0000 Subject: [PATCH] refactor: remove unnecessary `simp` call in `simpAppFn` and update `cbv_eval` attribute usage in tests (#12589) This PR removes unnecessary `simp` call in `simpAppFn` in `cbv` tactic and updates the usage of `cbv_eval` attribute in `tests/lean.run/cbv1.lean` to follow the new syntax that does not require an explicit name of the function for which we are registering the unfold lemma. --- src/Lean/Meta/Tactic/Cbv/Main.lean | 2 +- tests/lean/run/cbv1.lean | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Lean/Meta/Tactic/Cbv/Main.lean b/src/Lean/Meta/Tactic/Cbv/Main.lean index c67012a95d..fed44282d7 100644 --- a/src/Lean/Meta/Tactic/Cbv/Main.lean +++ b/src/Lean/Meta/Tactic/Cbv/Main.lean @@ -135,7 +135,7 @@ def simplifyAppFn : Simproc := fun e => do return .rfl else let res ← simp fn - match (← simp fn) with + match res with | .rfl _ => return res | .step e' proof _ => let newType ← Sym.inferType e' diff --git a/tests/lean/run/cbv1.lean b/tests/lean/run/cbv1.lean index f2af066280..af76b3cab6 100644 --- a/tests/lean/run/cbv1.lean +++ b/tests/lean/run/cbv1.lean @@ -176,8 +176,8 @@ attribute [cbv_opaque] Std.DHashMap.emptyWithCapacity attribute [cbv_opaque] Std.DHashMap.insert attribute [cbv_opaque] Std.DHashMap.getEntry attribute [cbv_opaque] Std.DHashMap.contains -attribute [cbv_eval Std.DHashMap.contains] Std.DHashMap.contains_emptyWithCapacity -attribute [cbv_eval Std.DHashMap.contains] Std.DHashMap.contains_insert +attribute [cbv_eval] Std.DHashMap.contains_emptyWithCapacity +attribute [cbv_eval] Std.DHashMap.contains_insert example : ((Std.DHashMap.emptyWithCapacity : Std.DHashMap Nat (fun _ => Nat)).insert 5 3).contains 5 = true := by conv =>