# Tests

```agda
{-# OPTIONS --rewriting --confluence-check #-}

module LC.Tests where

open import Notation
open import LC.Definitions
open Abstract-Syntax
open Domain-Equations
open Semantic-Functions

check-id : -- (λx1.x1)x42 = x42
  ⟦ ⦅ ⦅λ x 1 ␣ var x 1 ⦆ ␣ var x 42 ⦆ ⟧ ≡ ⟦ var x 42 ⟧
check-id = refl

check-const : -- (λx1.x42)x0 = x42
  ⟦ ⦅ ⦅λ x 1 ␣ var x 42 ⦆ ␣ var x 0 ⦆ ⟧ ≡ ⟦ var x 42 ⟧
check-const = refl 

-- check-divergence : -- (λx0.x0 x0)(λx0.x0 x0) = ...
--   ⟦ ⦅ ⦅λ x 0 ␣ ⦅ var x 0 ␣ var x 0 ⦆ ⦆ ␣ ⦅λ x 0 ␣ ⦅ var x 0 ␣ var x 0 ⦆ ⦆ ⦆ ⟧
--   ≡ ⟦ var x 42 ⟧
-- check-divergence = refl -- Agda type-checker diverges

check-convergence : -- (λx1.x42)((λx0.x0 x0)(λx0.x0 x0)) = x42
  ⟦  ⦅ ⦅λ x 1 ␣ var x 42 ⦆ ␣
     ⦅ ⦅λ x 0 ␣ ⦅ var x 0 ␣ var x 0 ⦆ ⦆ ␣ ⦅λ x 0 ␣ ⦅ var x 0 ␣ var x 0 ⦆ ⦆ ⦆ ⦆ ⟧
  ≡ ⟦ var x 42 ⟧
check-convergence = refl

check-abs : -- (λx1.x1)(λx1.x42) = λx2.x42
  ⟦ ⦅ ⦅λ x 1 ␣ var x 1 ⦆ ␣ ⦅λ x 1 ␣ var x 42 ⦆ ⦆ ⟧ ≡ ⟦ ⦅λ x 1 ␣ var x 42 ⦆ ⟧
check-abs = refl

check-free : -- (λx1.(λx42.x1)x2)x42 = x42
  ⟦ ⦅ ⦅λ x 1 ␣ ⦅ ⦅λ x 42 ␣ var x 1 ⦆ ␣ var x 2 ⦆ ⦆ ␣ var x 42 ⦆ ⟧ ≡ ⟦ var x 42 ⟧
check-free = refl
```