max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor: remove unnecessary simp call in simpAppFn and update cbv_eval attribute usage in tests (#12589)

Browse source 
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.
This commit is contained in:
Wojciech Różowski 2026-02-19 15:17:55 +00:00 • committed by GitHub
parent 953b60c894
commit d035efbb87
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Meta/Tactic/Cbv/Main.lean
View file

@ -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'

4
tests/lean/run/cbv1.lean
View file

@ -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 =>