diff options
Diffstat (limited to 'src/Cfe/Expression')
| -rw-r--r-- | src/Cfe/Expression/Base.agda | 4 | ||||
| -rw-r--r-- | src/Cfe/Expression/Properties.agda | 13 |
2 files changed, 15 insertions, 2 deletions
diff --git a/src/Cfe/Expression/Base.agda b/src/Cfe/Expression/Base.agda index 1cd57a7..aabab1b 100644 --- a/src/Cfe/Expression/Base.agda +++ b/src/Cfe/Expression/Base.agda @@ -100,5 +100,5 @@ rank (μ e) = suc (rank e) infix 4 _<ᵣₐₙₖ_ -_<ᵣₐₙₖ_ : ∀ {n} → Rel (Expression n) _ -_<ᵣₐₙₖ_ = ℕ._<_ on rank +_<ᵣₐₙₖ_ : ∀ {m n} → REL (Expression m) (Expression n) _ +e <ᵣₐₙₖ e′ = rank e ℕ.< rank e′ diff --git a/src/Cfe/Expression/Properties.agda b/src/Cfe/Expression/Properties.agda index d1e2869..f21fe72 100644 --- a/src/Cfe/Expression/Properties.agda +++ b/src/Cfe/Expression/Properties.agda @@ -231,3 +231,16 @@ e₂<ᵣₐₙₖe₁∨e₂ e₁ e₂ = begin-strict rank (e₁ ∨ e₂) ∎ where open ≤-Reasoning + +-- ⟦ e ⟧ (⟦ μ e ⟧ [] ∷ []) ≤ ⟦ μ e ⟧ [] +-- l ∈ ⟦ e ⟧ (⟦ μ e ⟧ [] ∷ []) → l ∈ ⟦ μ e ⟧ [] +-- l ∈ ⟦ e ⟧ (⟦ μ e ⟧ [] ∷ []) → l ∈ ⋃ (λ x → ⟦ e ⟧ (x ∷ [])) +-- l ∈ ⟦ e′ ⟧ (⟦ μ e ⟧ [] ∷ []) → ∃[ n ] l ∈ ⟦ e′ ⟧ ((λ X → ⟦ e ⟧ (X ∷ [])) ^ n ∷ []) +-- e-unroll : ∀ {n} (e : Expression (suc n)) e′ i γ → ⟦ e [ e′ / i ] ⟧ γ L.≤ ∃[ n ] (⟦ e ⟧ ) +-- e-unroll ⊥ = ? +-- e-unroll ε = ? +-- e-unroll (Char x) = ? +-- e-unroll (e ∨ e₁) = {!!} +-- e-unroll (e ∙ e₁) = {!!} +-- e-unroll (Var x) = {!!} +-- e-unroll (μ e) = {!!} |