lean4-htt/tests/elab/12457.lean
Wojciech Różowski 5cc6585c9b
chore: disable cbv usage warning (#12986)
This disables `cbv` usage warning and reflects that in the corresponding
unit tests.
2026-03-19 14:12:04 +00:00

1 line
89 B
Text

example : ("abc".pos ⟨1⟩ (by decide_cbv)).get (by decide_cbv) = 'b' := by decide_cbv