-- Copyright 2020 INP Toulouse. -- Authors : Mathieu Montin. -- This version of Tutorial is provided to you free of charge. It is released under the FSF GPL license, http://www.fsf.org/licenses/gpl.html. -- As a counterpart to the access to the source code and rights to copy, modify and redistribute granted by the license, users are provided only -- with a limited warranty and the software's author, the holder of the economic rights, and the successive licensors have only limited liability. -- In this respect, the user's attention is drawn to the risks associated with loading, using, modifying and/or developing or reproducing the -- software by the user in light of its specific status of free software, that may mean that it is complicated to manipulate, and that also there- -- fore means that it is reserved for developers and experienced professionals having in-depth computer knowledge. Users are therefore encouraged -- to load and test the software's suitability as regards their requirements in conditions enabling the security of their systems and/or data to -- be ensured and, more generally, to use and operate it in the same conditions as regards security. -- The fact that you are presently reading this means that you have had knowledge of the FSF GPL version 3 license and that you accept its terms. module Tutorial where data ℕ : Set where zero : ℕ suc : ℕ → ℕ data List {a} (A : Set a) : Set a where [] : List A _∷_ : A → List A → List A infixr 20 _∷_ data Vec {a} (A : Set a) : ℕ → Set a where [] : Vec A zero _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n) data Even : ℕ → Set where z-even : Even zero s-even : ∀ {n} → Even n → Even (suc (suc n)) six : ℕ six = suc (suc (suc (suc (suc (suc zero))))) 6-even : Even six 6-even = s-even (s-even (s-even z-even)) data dummy {a b} : Set a → Set b where _+_ : ℕ → ℕ → ℕ zero + b = b (suc a) + b = suc (a + b) size : ∀ {a} {A : Set a} → List A → ℕ size [] = zero size (hd ∷ tl) = suc (size tl) myList : List ℕ myList = zero ∷ [] sizeImp : ℕ sizeImp = size myList sizeExp : ℕ sizeExp = size {A = ℕ} myList _++_ : ∀ {a} {A : Set a} → List A → List A → List A [] ++ l = l (hd ∷ tl) ++ l = hd ∷ (tl ++ l) data _≡_ {a} {A : Set a} (x : A) : A → Set where refl : x ≡ x cong : ∀ {a b} {A : Set a} {B : Set b} {x y} (f : A → B) → x ≡ y → f x ≡ f y cong f refl = refl ≡size : ∀ {a} {A : Set a} {l l₁ : List A} → (size l + size l₁) ≡ size (l ++ l₁) ≡size {l = []} = refl ≡size {l = hd ∷ tl} = cong suc (≡size {l = tl}) _++̬_ : ∀ {n n₁ a} {A : Set a} → Vec A n → Vec A n₁ → Vec A (n + n₁) [] ++̬ v₂ = v₂ (x ∷ v₁) ++̬ v₂ = x ∷ (v₁ ++̬ v₂) data ⊥ : Set where ¬ : ∀ {a} → Set a → Set a ¬ A = A → ⊥ data Dec {a} (A : Set a) : Set a where yes : (p : A) → Dec A no : (¬p : ¬ A) → Dec A dec≡ : ∀ {x y : ℕ} → Dec (x ≡ y) dec≡ {zero} {zero} = yes refl dec≡ {zero} {suc y} = no (λ ()) dec≡ {suc x} {zero} = no (λ ()) dec≡ {suc x} {suc y} with dec≡ {x} {y} dec≡ {suc x} {suc y} | yes x≡y = yes (cong suc x≡y) dec≡ {suc x} {suc y} | no ¬x≡y = no (λ {refl → (¬x≡y refl)})