diff options
Diffstat (limited to 'src/Cfe/Type')
| -rw-r--r-- | src/Cfe/Type/Properties.agda | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/src/Cfe/Type/Properties.agda b/src/Cfe/Type/Properties.agda index 14e871b..987e41f 100644 --- a/src/Cfe/Type/Properties.agda +++ b/src/Cfe/Type/Properties.agda @@ -45,3 +45,26 @@ L⊨τ⊥⇒L≈∅ {L = L} L⊨τ⊥ = record ; f⇒f = λ () ; l⇒l = λ () } + +L⊨τε⇒L≤｛ε｝ : ∀ {a aℓ} {L : Language a aℓ} → L ⊨ τε → L ≤ ｛ε｝ +L⊨τε⇒L≤｛ε｝{L = L} L⊨τε = record + { f = λ {l} l∈L → elim l l∈L + ; cong = λ {l₁} {l₂} {l₁∈L} {l₂∈L} l₁≈l₂ → tt + } + where + open import Data.Unit + open import Relation.Binary.PropositionalEquality + module L⊨τε = _⊨_ L⊨τε + + elim : ∀ l (l∈L : l ∈ L) → l ∈ ｛ε｝ + elim [] []∈L = refl + elim (x ∷ l) xl∈L = ⊥-elim (L⊨τε.f⇒f (-, xl∈L)) + +｛ε｝⊨τε : ｛ε｝ ⊨ τε +｛ε｝⊨τε = record + { n⇒n = const tt + ; f⇒f = λ () + ; l⇒l = λ { ([] , ()) ; (_ ∷ _ , ())} + } + where + open import Data.Unit |