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 #-}