module Prim.Data.Maybe where
Primitive: The Maybe type🔗
The Maybe
is the free pointed type
on a given type. It is used by Agda’s primitives to represent
failure.
data Maybe {a} (A : Type a) : Type a where just : A → Maybe A nothing : Maybe A {-# BUILTIN MAYBE Maybe #-}