Function s

crates/compile/src/congruence.rs:417–419

(l: Level)

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