1{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness
2            --no-subtyping #-}
3
4module Agda.Builtin.Maybe where
5
6data Maybe {a} (A : Set a) : Set a where
7  just : A → Maybe A
8  nothing : Maybe A
9
10{-# BUILTIN MAYBE Maybe #-}
11