diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2021-01-23 21:23:04 +0000 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2021-01-23 21:23:04 +0000 |
| commit | 6385ceeb15670bfd3e059272e233c3d55bcb545b (patch) | |
| tree | ffe57d6ffa79b59f10a45af087c9532a9b6bf1aa /src/Cfe/Expression | |
| parent | 5c18d33d8e558068a9040c46ffc7bc17f34c29ef (diff) | |
Define expression equivalence.
Diffstat (limited to 'src/Cfe/Expression')
| -rw-r--r-- | src/Cfe/Expression/Base.agda | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/src/Cfe/Expression/Base.agda b/src/Cfe/Expression/Base.agda index 2a71422..4c53638 100644 --- a/src/Cfe/Expression/Base.agda +++ b/src/Cfe/Expression/Base.agda @@ -9,9 +9,11 @@ module Cfe.Expression.Base open Setoid setoid renaming (Carrier to A) open import Cfe.Language setoid renaming (_∙_ to _∙ₗ_) -open import Data.Fin -open import Data.Nat +open import Data.Fin hiding (_≤_) +open import Data.Nat hiding (_≤_; _⊔_) +open import Data.Product open import Data.Vec +open import Level renaming (suc to lsuc) data Expression : ℕ → Set a where ⊥ : {n : ℕ} → Expression n @@ -30,3 +32,6 @@ data Expression : ℕ → Set a where 〚 e₁ ∙ e₂ 〛 γ = 〚 e₁ 〛 γ ∙ₗ 〚 e₂ 〛 γ 〚 Var n 〛 γ = lookup γ n 〚 μ e 〛 γ = fix (λ X → 〚 e 〛 (X ∷ γ)) + +_≋_ : {n : ℕ} → Expression n → Expression n → Set (lsuc a ⊔ lsuc ℓ) +e₁ ≋ e₂ = ∀ γ → 〚 e₁ 〛 γ ≤ 〚 e₂ 〛 γ × 〚 e₂ 〛 γ ≤ 〚 e₁ 〛 γ |