From 6385ceeb15670bfd3e059272e233c3d55bcb545b Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Sat, 23 Jan 2021 21:23:04 +0000 Subject: Define expression equivalence. --- src/Cfe/Expression/Base.agda | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'src') 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₁ 〛 γ -- cgit v1.2.3