---
title: "Exercise 1"
order: 101
repo-actions: false
other-links:
  - text: Agda source
    icon: file-code
    href: ../_agda/CS410/Ex01.lagda.md
---

```agda
{-# OPTIONS --allow-unsolved-metas #-}

module CS410.Ex01 where

open import CS410.Prelude
open import CS410.Lec01
```

Prove that addition is associative.

```agda
+-assoc : ∀ l m n → (l + m) + n ≡ l + (m + n)
+-assoc l m n = {!!}
```