module Base where
infixr 1 _⊎_
infixr 2 _×_ _,_
data False : Set where
data Unit : Set where
unit : Unit
data Bool : Set where
false : Bool
true : Bool
{-# BUILTIN BOOL Bool #-}
{-# BUILTIN TRUE true #-}
{-# BUILTIN FALSE false #-}
data Maybe (A : Set) : Set where
nothing : Maybe A
just : A → Maybe A
record Σ (A : Set) (B : A → Set) : Set where
constructor _,_
field
fst : A
snd : B fst
open Σ public
syntax Σ A (λ a → B) = Σ[ a ∶ A ] B
_×_ : Set → Set → Set
A × B = Σ A (λ _ → B)
data _⊎_ (A B : Set) : Set where
inl : A → A ⊎ B
inr : B → A ⊎ B
Op : Set → Set
Op A = A → A → A