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