## Tutorial

- Introduction
- Monday 22 Nov 15:00 - 17:30, Original Completed Video
- Tuesday 23 Nov 15:00 - 16:30, Original Completed Video
- Wednesday 24 Nov 15:00 - 17:30, Original Completed Video
- Thursday 25 Nov 15:00 - 17:30, Original Completed Video

## Tutorials.Thursday

{-# OPTIONS --allow-unsolved-metas --guardedness #-} import Tutorials.Monday as Mon import Tutorials.Tuesday as Tue import Tutorials.Wednesday as Wed open Mon using (⊤; tt; ℕ; zero; suc) open Mon.Simple using (_⊎_; inl; inr) open Tue.Product using (Σ; _,_; fst; snd; _×_) module Tutorials.Thursday where variable A B C S : Set -- Things that we skipped so far -------------------------------- module WithAbstraction where open Mon using (Bool; true; false; Pred; _≡_; refl; _+_; subst; +-comm) open Mon.List using (List; []; _∷_) -- With abstraction -- You can use "with abstraction" to pattern match on intermediary computations -- These can be nested, or executed simultaneously filter : (A → Bool) → List A → List A filter f [] = [] filter f (x ∷ xs) with f x filter f (x ∷ xs) | true = x ∷ filter f xs filter f (x ∷ xs) | false = filter f xs -- Alternative notation filter′ : (A → Bool) → List A → List A filter′ f [] = [] filter′ f (x ∷ xs) with f x ... | true = x ∷ filter′ f xs ... | false = filter′ f xs -- The goal type and the type of the arguments are generalised over the value of the scrutinee thm : {P : Pred ℕ} (n m : ℕ) → P (n + m) → P (m + n) -- 1) Here (p : P (n + m)) and (eq : n + m ≡ m + n) -- thm n m p with +-comm n m -- thm n m p | eq = {!!} -- 2) Here (p : P x) and (eq : x ≡ m + n) -- thm n m p with n + m | +-comm n m -- thm n m p | x | eq = {!!} -- 3) Pattern matching we get (p : P (m + n)), the dot signifies that the argument is uniquely determined thm n m p with n + m | +-comm n m thm n m p | .(m + n) | refl = p -- This is such a common formula that there is special syntax for it thm′ : {P : Pred ℕ} (n m : ℕ) → P (n + m) → P (m + n) thm′ n m p rewrite +-comm n m = p -- We could use subst to be more explicit about *where* the rewrite happens thm′′ : {P : Pred ℕ} (n m : ℕ) → P (n + m) → P (m + n) thm′′ {P} n m p = subst {P = P} (+-comm n m) p -- A little on coinductive types -------------------------------- -- Stolen from https://github.com/pigworker/CS410-17/blob/master/lectures/Lec6Done.agda ListT : Set → Set → Set ListT X B = ⊤ ⊎ (X × B) module List where data List (A : Set) : Set where [] : List A _∷_ : A → List A → List A mkList : ListT A (List A) → List A mkList x = {!!} foldr : (ListT A B → B) → List A → B foldr alg xs = {!!} list-id : List A → List A list-id = {!!} incr : ListT A ℕ → ℕ incr x = {!!} length : List A → ℕ length = {!!} module CoList where record CoList (A : Set) : Set where coinductive field next : ListT A (CoList A) open CoList [] : CoList A [] = {!!} _∷_ : A → CoList A → CoList A (x ∷ xs) = {!!} unfoldr : (S → ListT A S) → S → CoList A unfoldr coalg s = {!!} colist-id : CoList A → CoList A colist-id = {!!} repeat : A → CoList A repeat = {!!} take : ℕ → CoList A → List.List A take n xs = {!!} module Stream where record Stream (A : Set) : Set where coinductive field head : A tail : Stream A open Stream forever : A → Stream A forever x = {!!} unfold : (S → A × S) → S → Stream A unfold coalg s = {!!} --------------------------------------------- -- If you are interested in more -- Documentation for Agda: https://agda.readthedocs.io/en/v2.6.0.1/index.html -- Programming Language Foundations in Agda: https://plfa.github.io/ -- Lots of other nice tutorials online -- The standard library: https://agda.github.io/agda-stdlib/