max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/tests/pkg/cbv_attr/CbvAttr
History
Exact
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
..
InvertedLocalTheorem.lean chore: disable cbv usage warning (#12986) 2026-03-19 14:12:04 +00:00
InvertedTheorem.lean chore: disable cbv usage warning (#12986) 2026-03-19 14:12:04 +00:00
PublicFunction.lean
PublicFunctionLocalTheorem.lean chore: disable cbv usage warning (#12986) 2026-03-19 14:12:04 +00:00
PublicFunctionPrivateTheorem.lean chore: disable cbv usage warning (#12986) 2026-03-19 14:12:04 +00:00
PubliclyVisibleTheorem.lean chore: disable cbv usage warning (#12986) 2026-03-19 14:12:04 +00:00
Tst.lean chore: disable cbv usage warning (#12986) 2026-03-19 14:12:04 +00:00