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