Function im

crates/compile/src/congruence.rs:426–428

Raw `Level::imax`.

(x: Level, y: Level)

  }
  /// Raw `Level::imax`.
  fn im(x: Level, y: Level) -> Level {
    Level::imax(x, y)
  }

  /// `max(a, a) = a` — the canonical aux_gen vs Lean divergence on
  /// nested-aux level args from `ec95312` (the `Sort (max 1 1)` vs