exportLevel — Mathlib

Lean4
def exportLevel (L : Level) : ExportM Nat := do
  match (← get).levels.map[L]? with
  | some i =>
    pure i
  | none =>
    match L with
    | .zero =>
      pure 0
    | .succ l =>
      let i ← alloc L;
      IO.println s! "{i} #US {← exportLevel l}";
      pure i
    | .max l₁ l₂ =>
      let i ← alloc L;
      IO.println s! "{i} #UM {(← exportLevel l₁)} {← exportLevel l₂}";
      pure i
    | .imax l₁ l₂ =>
      let i ← alloc L;
      IO.println s! "{i} #UIM {(← exportLevel l₁)} {← exportLevel l₂}";
      pure i
    | .param n =>
      let i ← alloc L;
      IO.println s! "{i} #UP {← exportName n}";
      pure i
    | .mvar _ =>
      unreachable!
Похожие утверждения