/Prelude-v20.0.0/Function/identity.dhall

Copy path to clipboard

The identity function simply returns its input

Examples

identity Natural 1 ≡ 1
identity Bool ≡ (λ(x : Bool) → x)

Source

--| The identity function simply returns its input
let identity
: ∀(a : Type) → ∀(x : a) → a
= λ(a : Type) → λ(x : a) → x

let example0 = assert : identity Natural 1 ≡ 1

let example1 = assert : identity Bool ≡ (λ(x : Bool) → x)

in identity