fix: remove grind attr from Xi.step_lc_r by lengyijun · Pull Request #751 · leanprover/cslib

lengyijun · 2026-07-26T00:46:31Z

We have grind attr for FullBeta.step_lc_r and FullEta.step_lc_r already.
grind never use Xi.step_lc_r

lengyijun requested review from chenson2018 and fmontesi as code owners July 26, 2026 00:46

lengyijun force-pushed the not_grind_step_lc_r branch from 49ce90c to 42cd7cc Compare August 23, 2026 23:01

lengyijun force-pushed the not_grind_step_lc_r branch from 42cd7cc to 44a4232 Compare September 16, 2026 05:07

lengyijun requested review from arademaker, kim-em and sorrachai as code owners September 16, 2026 05:07

lengyijun force-pushed the not_grind_step_lc_r branch 2 times, most recently from 870b4da to 7352449 Compare September 21, 2026 23:47

lengyijun requested a review from SamuelSchlesinger as a code owner September 21, 2026 23:47

lengyijun force-pushed the not_grind_step_lc_r branch 3 times, most recently from 24ab56a to 97464dc Compare September 28, 2026 00:14

lengyijun force-pushed the not_grind_step_lc_r branch 2 times, most recently from 52119d0 to 6e5db2f Compare October 5, 2026 00:29

lengyijun requested a review from crei as a code owner October 5, 2026 00:29

lengyijun force-pushed the not_grind_step_lc_r branch 3 times, most recently from 767cf71 to 2e3c785 Compare October 14, 2026 04:56

fix: remove grind attr from Xi.step_lc_r

6b8aae0

lengyijun force-pushed the not_grind_step_lc_r branch from 2e3c785 to 6b8aae0 Compare October 17, 2026 00:20

Navigation Menu