sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 18:34:06 +00:00
Code Issues Packages Projects Releases Wiki Activity

test: add regression test for List.length implicit reducibility

Browse Source 
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
This commit is contained in:
Leonardo de Moura
2026-03-15 01:27:05 +00:00
parent 38c4fd4afd
commit 9661c3ab67
2 changed files with 14 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

13
tests/elab/implicit_reducible_list_length.lean Normal file
View File

@@ -0,0 +1,13 @@
/-!
Regression test: `simp` should be able to apply lemmas that depend on `List.length`
even when `List.length` appears inside implicit type class instance arguments.
See https://github.com/leanprover/lean4/pull/12924
-/
theorem BitVec.getElem!_eq_testBit_toNat {w : Nat} (x : BitVec w) (i : Nat) :
x[i]! = x.toNat.testBit i := by sorry
example (l : List Nat) (a : Nat) (j : Nat) :
(0#((a :: l).length))[j]! = (0#((a :: l).length)).toNat.testBit j := by
simp only [List.length_cons]
simp only [BitVec.getElem!_eq_testBit_toNat]

1
tests/elab/implicit_reducible_list_length.lean.out.expected Normal file
View File

@@ -0,0 +1 @@
implicit_reducible_list_length.lean:7:8-7:40: warning: declaration uses `sorry`