From 8abb1b5601fabf5e7560d08faa6e633e60663e0a Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 29 Apr 2021 20:58:04 +0100
Subject: Finally prove that e [ μ e / zero ] ≈ μ e.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Complete proof of generator.
---
 src/Cfe/Expression/Base.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src/Cfe/Expression/Base.agda')

diff --git a/src/Cfe/Expression/Base.agda b/src/Cfe/Expression/Base.agda
index f37694b..933b3bb 100644
--- a/src/Cfe/Expression/Base.agda
+++ b/src/Cfe/Expression/Base.agda
@@ -46,7 +46,7 @@ infix 4 _≈_
 ⟦ Char x ⟧  _ = ｛ x ｝
 ⟦ e₁ ∨ e₂ ⟧ γ = ⟦ e₁ ⟧ γ ∪ ⟦ e₂ ⟧ γ
 ⟦ e₁ ∙ e₂ ⟧ γ = ⟦ e₁ ⟧ γ ∙ˡ ⟦ e₂ ⟧ γ
-⟦ Var n ⟧   γ = lookup γ n
+⟦ Var j ⟧   γ = lookup γ j
 ⟦ μ e ⟧     γ = ⋃ (λ X → ⟦ e ⟧ (X ∷ γ))
 
 _≈_ : {n : ℕ} → Expression n → Expression n → Set _
-- 
cgit v1.2.3