Function m

crates/compile/src/congruence.rs:422–424

Raw `Level::max` (no simplification) — what Lean's exporter and `Level.instantiateParams` produce.

(x: Level, y: Level)

  /// Raw `Level::max` (no simplification) — what Lean's exporter and
  /// `Level.instantiateParams` produce.
  fn m(x: Level, y: Level) -> Level {
    Level::max(x, y)
  }
  /// Raw `Level::imax`.
  fn im(x: Level, y: Level) -> Level {
    Level::imax(x, y)