diff options
Diffstat (limited to 'src/Cfe')
| -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₁ 〛 γ |