open import Prim.Type open import Prim.Kan 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 #-}