open import Agda.Builtin.Equality -- Agda: The substance of the matrix. -- A framework where things can be defined. -- Set of natural numbers data ℕ : Set where zero : ℕ suc : (n : ℕ) → ℕ one = suc zero two = suc one three = suc two -- Set of natural number below a fixed number n data Below : (n : ℕ) → Set where zero : ∀{n} → Below (suc n) suc : ∀{n} → (i : Below n) → Below (suc n) -- Set of lists whose elements are in A data List A : (n : ℕ) → Set where [] : List A zero _∷_ : ∀{n} (head : A) (tail : List A n) → List A (suc n) infixr 10 _∷_ l123 : List ℕ (suc (suc (suc zero))) l123 = one ∷ two ∷ three ∷ [] -- Increase every list element by one incr : ∀{n} → List ℕ n → List ℕ n incr [] = [] incr (head ∷ l) = suc head ∷ incr l test = incr l123 -- Get the ith element of list l lookup : ∀{A n} (l : List A n) (i : Below n) → A lookup [] () lookup (head ∷ l) zero = head lookup (head ∷ l) (suc i) = lookup l i -- Theorem: lookup after incr = suc after lookup lookup-incr : ∀{n} (l : List ℕ n) (i : Below n) → lookup (incr l) i ≡ suc (lookup l i) lookup-incr [] () lookup-incr (head ∷ l) zero = refl lookup-incr (head ∷ l) (suc i) = lookup-incr l i -- -}