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

@[implicit_reducible, always_inline]

instance Id.instMonad : Monad Id

@[implicit_reducible]

def Id.hasBind : Bind Id

The identity monad has a bind operator.

@[implicit_reducible, 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.

@[implicit_reducible]

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

@[implicit_reducible]

instance Id.instMonadLiftTOfPure {m : Type u → Type v} [Pure m] : MonadLiftT Id m

@[implicit_reducible]

instance Id.instMonadAttach : MonadAttach Id

instance Id.instLawfulMonadAttach : LawfulMonadAttach Id

def ForIn.toArray {ρ : Type u_1} {α : Type u} [inst : ForIn Id ρ α] (xs : ρ) : Array α

Turn a collection with a pure ForIn instance into an array.

def ForIn.toList {ρ : Type u_1} {α : Type u} [ForIn Id ρ α] (xs : ρ) : List α

Turn a collection with a pure ForIn instance into a list.