repos / bachelor-thesis.git

Prelude.agda

 1module Prelude where
 2
 3open import Data.Empty
 4open import Function
 5open import Level using (_⊔_)
 6open import Relation.Binary.PropositionalEquality using (_≡_; refl; setoid) public
 7
 8open import Agda.Builtin.List public
 9  using (List; []; _∷_)
10
11¬_ : ∀ {ℓ} → Set ℓ → Set ℓ
12¬ P = P → ⊥
13
14data Bool : Set where
15  true false : Bool
16  
17data String : Set where
18
19open import Agda.Builtin.Nat public
20  using    ( zero; suc; _+_; _*_ )
21  renaming ( Nat to ℕ
22           ; _-_ to _∸_ )
23
24open import Agda.Builtin.Int public
25  using ()
26  renaming ( Int to ℤ
27           ; negsuc to -[1+_]  -- -[1+ n ] stands for - (1 + n).
28           ; pos    to +_ )
29
30
31infixr 5 _∷_
32data Vec {a} (A : Set a) : ℕ → Set a where
33  []  : Vec A zero
34  _∷_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (suc n)
35
36infix 4 _∈-Vec_
37
38data _∈-Vec_ {a} {A : Set a} : A → {n : ℕ} → Vec A n → Set a where
39  here  : ∀ {n} {x}   {xs : Vec A n} → x ∈-Vec x ∷ xs
40  there : ∀ {n} {x y} {xs : Vec A n} (x∈xs : x ∈-Vec xs) → x ∈-Vec y ∷ xs
41
42toList : ∀ {a n} {A : Set a} → Vec A n → List A
43toList []       = List.[]
44toList (x ∷ xs) = List._∷_ x (toList xs)
45
46infixr 4 _,_
47infixr 2 _×_
48record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
49  constructor _,_
50  field
51    proj₁ : A
52    proj₂ : B proj₁
53
54infix 2 Σ-syntax
55
56Σ-syntax : ∀ {a b} (A : Set a) → (A → Set b) → Set (a ⊔ b)
57Σ-syntax = Σ
58
59syntax Σ-syntax A (λ x → B) = Σ[ x ∈ A ] B
60
61∃ : ∀ {a b} {A : Set a} → (A → Set b) → Set (a ⊔ b)
62∃ = Σ _
63
64∃-syntax : ∀ {a b} {A : Set a} → (A → Set b) → Set (a ⊔ b)
65∃-syntax = ∃
66
67syntax ∃-syntax (λ x → B) = ∃[ x ] B
68
69_×_ : ∀ {a b} (A : Set a) (B : Set b) → Set (a ⊔ b)
70A × B = Σ[ x ∈ A ] B