diff options
Diffstat (limited to 'src/Cfe/Expression/Base.agda')
| -rw-r--r-- | src/Cfe/Expression/Base.agda | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/src/Cfe/Expression/Base.agda b/src/Cfe/Expression/Base.agda index c4940b6..f4a8dc0 100644 --- a/src/Cfe/Expression/Base.agda +++ b/src/Cfe/Expression/Base.agda @@ -15,11 +15,12 @@ open import Cfe.Language.Construct.Concatenate over renaming (_∙_ to _∙ₗ_) open import Cfe.Language.Construct.Single over open import Cfe.Language.Construct.Union over open import Cfe.Language.Indexed.Construct.Iterate over -open import Data.Fin as F hiding (_≤_) +open import Data.Fin as F hiding (_≤_; cast) open import Data.Nat as ℕ hiding (_≤_; _⊔_) open import Data.Product open import Data.Vec open import Level renaming (suc to lsuc) hiding (Lift) +open import Relation.Binary.PropositionalEquality open import Relation.Nullary infix 10 _[_/_] @@ -36,6 +37,15 @@ data Expression : ℕ → Set c where Var : ∀ {n} → Fin n → Expression n μ : ∀ {n} → Expression (suc n) → Expression n +cast : ∀ {m n} → .(_ : m ≡ n) → Expression m → Expression n +cast eq ⊥ = ⊥ +cast eq ε = ε +cast eq (Char x) = Char x +cast eq (e₁ ∨ e₂) = cast eq e₁ ∨ cast eq e₂ +cast eq (e₁ ∙ e₂) = cast eq e₁ ∙ cast eq e₂ +cast eq (Var i) = Var (F.cast eq i) +cast eq (μ e) = μ (cast (cong suc eq) e) + wkn : ∀ {n} → Expression n → Fin (suc n) → Expression (suc n) wkn ⊥ i = ⊥ wkn ε i = ε |