Theoria.Level (theoria v0.7.0)

Universe levels.

Summary

subst()

t()

cast!(level)

max(left, right)

normalize(level)

param(name)

params(level)

succ(level)

zero()

zero?(level)

@type subst() :: %{optional(atom()) => t()}

@type t() ::
  Theoria.Level.Zero.t()
  | Theoria.Level.Succ.t()
  | Theoria.Level.Max.t()
  | Theoria.Level.Param.t()

@spec cast!(non_neg_integer() | t()) :: t()

@spec equal?(t(), t()) :: boolean()

@spec from_integer(non_neg_integer()) :: t()

@spec leq?(t(), t()) :: boolean()

@spec max(t(), t()) :: t()

@spec normalize(t()) :: t()

@spec param(atom()) :: Theoria.Level.Param.t()

@spec params(t()) :: MapSet.t(atom())

@spec subst(t(), subst()) :: t()

@spec succ(t()) :: Theoria.Level.Succ.t()

@spec to_integer(t()) :: {:ok, non_neg_integer()} | :error

@spec zero() :: Theoria.Level.Zero.t()

@spec zero?(t()) :: boolean()