def Id (type : Type u) : Type u

The identity function on types, used primarily for its Monad instance.

The identity monad is useful together with monad transformers to construct monads for particular purposes. Additionally, it can be used with do-notation in order to use control structures such as local mutability, for-loops, and early returns in code that does not otherwise use monads.

Examples:

def containsFive (xs : List Nat) : Bool := Id.run do
  for x in xs do
    if x == 5 then return true
  return false

#eval containsFive [1, 3, 5, 7]

true

Equations

• Id type = type

@[always_inline]

instance Id.instMonad : Monad Id

Equations

• One or more equations did not get rendered due to their size.

def Id.hasBind : Bind Id

The identity monad has a bind operator.

Equations

• Id.hasBind = inferInstance

@[inline]

def Id.run {α : Type u_1} (x : Id α) : α

Runs a computation in the identity monad.

This function is the identity function. Because its parameter has type Id α, it causes do-notation in its arguments to use the Monad Id instance.

Equations

• x.run = x

instance Id.instOfNat {α : Type u_1} {n : Nat} [OfNat α n] : OfNat (Id α) n

Equations

• Id.instOfNat = inferInstanceAs (OfNat α n)