diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2021-04-29 20:58:04 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2021-04-29 20:58:04 +0100 |
| commit | 8abb1b5601fabf5e7560d08faa6e633e60663e0a (patch) | |
| tree | 99e76379b280cc16bc869830ba3a3b89e5c99c12 /src/Cfe/Expression/Base.agda | |
| parent | 0708355c7988345c98961cad087dc56eeb16ea7f (diff) | |
Finally prove that e [ μ e / zero ] ≈ μ e.
Complete proof of generator.
Diffstat (limited to 'src/Cfe/Expression/Base.agda')
| -rw-r--r-- | src/Cfe/Expression/Base.agda | 2 |
1 files changed, 1 insertions, 1 deletions
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 _ |