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