Lean.InternalExceptionId

Type

Equations

Equations

Equations

Lean.registerInternalExceptionId name = do let exs ← ST.Ref.get Lean.internalExceptionsRef let _do_jp : PUnit → IO Lean.InternalExceptionId := fun y => let nextIdx := Array.size exs; do ST.Ref.modify Lean.internalExceptionsRef fun a => Array.push a name pure { idx := nextIdx } if Array.contains exs name = true then do let y ← throw (IO.userError (toString "invalid internal exception id, '" ++ toString name ++ toString "' has already been used")) _do_jp y else do let y ← pure PUnit.unit _do_jp y

Equations

Equations

Lean.InternalExceptionId.getName id = do let exs ← ST.Ref.get Lean.internalExceptionsRef let i : Nat := id.idx if h : i < Array.size exs then pure (Array.get exs { val := i, isLt := h }) else throw (IO.userError "invalid internal exception id")