`Qround.v`: Add more rounding functions - #291

Open

RyanGlScott wants to merge 8 commits into

rocq-prover:masterfrom

RyanGlScott:T283-more-rounding-functions

Commits on Jul 15, 2026

Qround.v: Add some documentation for Qfloor and Qceiling
RyanGlScott
committed
2b33d18
QArith_base.v: Add Qle_bool_imp_gt
RyanGlScott
committed
1d1de25
Qround.v: Add Qtruncate and related properties
RyanGlScott
committed
3c462ac
Qround.v: Add Q{floor,truncate}_frac_part and related properties
RyanGlScott
committed
3b6db7d
Qround.v: Add Q{floor,ceiling}_add_Z_{l,r}
RyanGlScott
committed
19bf634
Qround.v: Add Qround_away and related properties
RyanGlScott
committed
df610d6
Qround.v: Add Qround_to_even and related properties
RyanGlScott
committed
6d651e4
Regenerate theories/All.v
RyanGlScott
committed
19b9c4d