{-# OPTIONS --without-K #-}
module Prelude where
open import Agda.Primitive public using (Level; _⊔_; lzero; lsuc)
record ↑ {a} ℓ (A : Set a) : Set (a ⊔ ℓ) where
constructor lift
field lower : A
open ↑ public
record ⊤ : Set where
constructor tt
data ⊥ {ℓ} : Set ℓ where
⊥-elim : ∀ {w ℓ} {Whatever : Set w} → ⊥ {ℓ = ℓ} → Whatever
⊥-elim ()
⊥₀ : Set
⊥₀ = ⊥
infix 3 ¬_
¬_ : ∀ {ℓ} → Set ℓ → Set ℓ
¬ P = P → ⊥₀
data ℕ : Set where
zero : ℕ
suc : (n : ℕ) → ℕ
{-# BUILTIN NATURAL ℕ #-}
ℕ-rec : ∀ {p} {P : ℕ → Set p} →
P 0 → (∀ n → P n → P (suc n)) → ∀ n → P n
ℕ-rec z s zero = z
ℕ-rec z s (suc n) = s n (ℕ-rec z s n)
infixl 6 _+_
_+_ : ℕ → ℕ → ℕ
zero + n = n
suc m + n = suc (m + n)
infixl 7 _*_
_*_ : ℕ → ℕ → ℕ
zero * n = zero
suc m * n = n + m * n
infixr 8 _^_
_^_ : ℕ → ℕ → ℕ
m ^ zero = 1
m ^ suc n = m * m ^ n
infix 9 _!
_! : ℕ → ℕ
zero ! = 1
suc n ! = suc n * n !
# : ℕ → Level
# zero = lzero
# (suc n) = lsuc (# n)
infixr 9 _∘_
infixl 1 _on_
infixr 0 _$_
id : ∀ {a} {A : Set a} → A → A
id x = x
_∘_ : ∀ {a b c}
{A : Set a} {B : A → Set b} {C : {x : A} → B x → Set c} →
(∀ {x} (y : B x) → C y) → (g : (x : A) → B x) →
((x : A) → C (g x))
f ∘ g = λ x → f (g x)
_$_ : ∀ {a b} {A : Set a} {B : A → Set b} →
((x : A) → B x) → ((x : A) → B x)
f $ x = f x
const : ∀ {a b} {A : Set a} {B : Set b} → A → (B → A)
const x = λ _ → x
{-# DISPLAY const x y = x #-}
flip : ∀ {a b c} {A : Set a} {B : Set b} {C : A → B → Set c} →
((x : A) (y : B) → C x y) → ((y : B) (x : A) → C x y)
flip f = λ x y → f y x
_on_ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} →
(B → B → C) → (A → B) → (A → A → C)
_*_ on f = λ x y → f x * f y
Type-of : ∀ {a} {A : Set a} → A → Set a
Type-of {A = A} _ = A
infixr 4 _,_
infixr 2 _×_
record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
constructor _,_
field
proj₁ : A
proj₂ : B proj₁
open Σ public
∃ : ∀ {a b} {A : Set a} → (A → Set b) → Set (a ⊔ b)
∃ = Σ _
_×_ : ∀ {a b} (A : Set a) (B : Set b) → Set (a ⊔ b)
A × B = Σ A (const B)
Σ-map : ∀ {a b p q}
{A : Set a} {B : Set b} {P : A → Set p} {Q : B → Set q} →
(f : A → B) → (∀ {x} → P x → Q (f x)) →
Σ A P → Σ B Q
Σ-map f g = λ p → (f (proj₁ p) , g (proj₂ p))
Σ-zip : ∀ {a b c p q r}
{A : Set a} {B : Set b} {C : Set c}
{P : A → Set p} {Q : B → Set q} {R : C → Set r} →
(f : A → B → C) → (∀ {x y} → P x → Q y → R (f x y)) →
Σ A P → Σ B Q → Σ C R
Σ-zip f g = λ p q → (f (proj₁ p) (proj₁ q) , g (proj₂ p) (proj₂ q))
curry : ∀ {a b c} {A : Set a} {B : A → Set b} {C : Σ A B → Set c} →
((p : Σ A B) → C p) →
((x : A) (y : B x) → C (x , y))
curry f x y = f (x , y)
uncurry : ∀ {a b c} {A : Set a} {B : A → Set b} {C : Σ A B → Set c} →
((x : A) (y : B x) → C (x , y)) →
((p : Σ A B) → C p)
uncurry f (x , y) = f x y
data W {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
sup : (x : A) (f : B x → W A B) → W A B
head : ∀ {a b} {A : Set a} {B : A → Set b} →
W A B → A
head (sup x f) = x
tail : ∀ {a b} {A : Set a} {B : A → Set b} →
(x : W A B) → B (head x) → W A B
tail (sup x f) = f
abstract
inhabited⇒W-empty : ∀ {a b} {A : Set a} {B : A → Set b} →
(∀ x → B x) → ¬ W A B
inhabited⇒W-empty b (sup x f) = inhabited⇒W-empty b (f (b x))
{-# BUILTIN SIZEUNIV Size-universe #-}
{-# BUILTIN SIZE Size #-}
{-# BUILTIN SIZELT Size<_ #-}
{-# BUILTIN SIZESUC ssuc #-}
{-# BUILTIN SIZEINF ∞ #-}
infixr 1 _⊎_
data _⊎_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
inj₁ : (x : A) → A ⊎ B
inj₂ : (y : B) → A ⊎ B
[_,_] : ∀ {a b c} {A : Set a} {B : Set b} {C : A ⊎ B → Set c} →
((x : A) → C (inj₁ x)) → ((x : B) → C (inj₂ x)) →
((x : A ⊎ B) → C x)
[ f , g ] (inj₁ x) = f x
[ f , g ] (inj₂ y) = g y
⊎-map : ∀ {a₁ a₂ b₁ b₂}
{A₁ : Set a₁} {A₂ : Set a₂} {B₁ : Set b₁} {B₂ : Set b₂} →
(A₁ → A₂) → (B₁ → B₂) → A₁ ⊎ B₁ → A₂ ⊎ B₂
⊎-map f g = [ inj₁ ∘ f , inj₂ ∘ g ]
From-⊎ : ∀ {ℓ} {A B : Set ℓ} → A ⊎ B → Set ℓ
From-⊎ {A = A} (inj₁ _) = A
From-⊎ {B = B} (inj₂ _) = B
from-⊎ : ∀ {ℓ} {A B : Set ℓ} (x : A ⊎ B) → From-⊎ x
from-⊎ (inj₁ x) = x
from-⊎ (inj₂ y) = y
Dec : ∀ {p} → Set p → Set p
Dec P = P ⊎ ¬ P
pattern yes p = inj₁ p
pattern no p = inj₂ p
Decidable : ∀ {a b ℓ} {A : Set a} {B : Set b} →
(A → B → Set ℓ) → Set (a ⊔ b ⊔ ℓ)
Decidable _∼_ = ∀ x y → Dec (x ∼ y)
infixr 1 _Xor_
_Xor_ : ∀ {a b} → Set a → Set b → Set (a ⊔ b)
A Xor B = (A × ¬ B) ⊎ (¬ A × B)
Maybe : ∀ {a} → Set a → Set a
Maybe A = ⊤ ⊎ A
pattern nothing = inj₁ tt
pattern just x = inj₂ x
Bool : Set
Bool = ⊤ ⊎ ⊤
pattern true = inj₁ tt
pattern false = inj₂ tt
if_then_else_ : ∀ {a} {A : Set a} → Bool → A → A → A
if true then t else f = t
if false then t else f = f
not : Bool → Bool
not b = if b then false else true
infixr 6 _∧_
_∧_ : Bool → Bool → Bool
b₁ ∧ b₂ = if b₁ then b₂ else false
infixr 5 _∨_
_∨_ : Bool → Bool → Bool
b₁ ∨ b₂ = if b₁ then true else b₂
T : Bool → Set
T b = if b then ⊤ else ⊥
infixr 5 _∷_
data List {a} (A : Set a) : Set a where
[] : List A
_∷_ : (x : A) (xs : List A) → List A
foldr : ∀ {a b} {A : Set a} {B : Set b} →
(A → B → B) → B → List A → B
foldr _⊕_ ε [] = ε
foldr _⊕_ ε (x ∷ xs) = x ⊕ foldr _⊕_ ε xs
length : ∀ {a} {A : Set a} → List A → ℕ
length = foldr (const suc) 0
infixr 5 _++_
_++_ : ∀ {a} {A : Set a} → List A → List A → List A
xs ++ ys = foldr _∷_ ys xs
map : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → List A → List B
map f = foldr (λ x ys → f x ∷ ys) []
concat : ∀ {a} {A : Set a} → List (List A) → List A
concat = foldr _++_ []
infixl 5 _>>=_
_>>=_ : ∀ {a b} {A : Set a} {B : Set b} →
List A → (A → List B) → List B
xs >>= f = concat (map f xs)
filter : ∀ {a} {A : Set a} → (A → Bool) → List A → List A
filter p = foldr (λ x xs → if p x then x ∷ xs else xs) []
Fin : ℕ → Set
Fin zero = ⊥
Fin (suc n) = ⊤ ⊎ Fin n
pattern fzero = inj₁ tt
pattern fsuc i = inj₂ i
lookup : ∀ {a} {A : Set a} (xs : List A) → Fin (length xs) → A
lookup [] ()
lookup (x ∷ xs) fzero = x
lookup (x ∷ xs) (fsuc i) = lookup xs i
_→-rel_ : ∀ {a b c d ℓ}
{A : Set a} {B : Set b} {C : Set c} {D : Set d} →
(A → C → Set ℓ) → (B → D → Set ℓ) →
(A → B) → (C → D) → Set (a ⊔ c ⊔ ℓ)
(P →-rel Q) f g = ∀ x y → P x y → Q (f x) (g y)
_×-rel_ : ∀ {a b c d ℓ}
{A : Set a} {B : Set b} {C : Set c} {D : Set d} →
(A → C → Set ℓ) → (B → D → Set ℓ) → A × B → C × D → Set ℓ
(P ×-rel Q) (x , u) (y , v) = P x y × Q u v
_⊎-rel_ : ∀ {a b c d ℓ}
{A : Set a} {B : Set b} {C : Set c} {D : Set d} →
(A → C → Set ℓ) → (B → D → Set ℓ) → A ⊎ B → C ⊎ D → Set ℓ
(P ⊎-rel Q) (inj₁ x) (inj₁ y) = P x y
(P ⊎-rel Q) (inj₁ x) (inj₂ v) = ⊥
(P ⊎-rel Q) (inj₂ u) (inj₁ y) = ⊥
(P ⊎-rel Q) (inj₂ u) (inj₂ v) = Q u v