Construct `imax(a, b)` with Lean-style simplifications: - `imax(a, b) = max(a, b)` when `b` is never zero - `imax(a, 0) = 0` - `imax(0, b) = b`, `imax(1, b) = b` - `imax(a, a) = a` Matches Lean's `mk_imax` in `kernel/level.cpp:112-120`.
(a: KUniv<M>, b: KUniv<M>)
| 209 | Self::max_raw(a, b) |
| 210 | } |
| 211 | |
| 212 | /// Raw `Max` constructor without simplification. Used by `max()` after |
| 213 | /// all simplification opportunities are exhausted. |
| 214 | fn max_raw(a: KUniv<M>, b: KUniv<M>) -> Self { |
| 215 | KUniv::new(UnivData::Max(a, b, super::expr::fresh_uid())) |
| 216 | } |
| 217 | |
| 218 | /// Construct `imax(a, b)` with Lean-style simplifications: |
| 219 | /// |
| 220 | /// - `imax(a, b) = max(a, b)` when `b` is never zero |
| 221 | /// - `imax(a, 0) = 0` |
| 222 | /// - `imax(0, b) = b`, `imax(1, b) = b` |
| 223 | /// - `imax(a, a) = a` |
| 224 | /// |
| 225 | /// Matches Lean's `mk_imax` in `kernel/level.cpp:112-120`. |
| 226 | pub fn imax(a: KUniv<M>, b: KUniv<M>) -> Self { |
| 227 | if b.is_never_zero() { |
| 228 | return Self::max(a, b); |
| 229 | } |
| 230 | if b.is_zero() { |
| 231 | return b; // imax(a, 0) = 0 |
| 232 | } |
| 233 | if a.is_zero() { |
| 234 | return b; // imax(0, b) = b |
| 235 | } |
| 236 | // imax(1, b) = b (Lean: is_one check) |
| 237 | if let UnivData::Succ(inner, _) = a.data() |
| 238 | && inner.is_zero() |
| 239 | { |