Wojciech Różowski 7d32030729 feat: add cbv_eval attribute (#12296) ... This PR adds `cbv_eval` attribute that allows to evaluate functions in `cbv` tactic using pre-registered theorems.		2026-02-10 15:41:42 +00:00
..
CbvAttr
CbvAttr.lean
lakefile.lean
lean-toolchain
test.sh