diff options
Diffstat (limited to 'src/Cfe/Parse')
| -rw-r--r-- | src/Cfe/Parse/Base.agda | 23 | ||||
| -rw-r--r-- | src/Cfe/Parse/Properties.agda | 7 |
2 files changed, 30 insertions, 0 deletions
diff --git a/src/Cfe/Parse/Base.agda b/src/Cfe/Parse/Base.agda new file mode 100644 index 0000000..50e085a --- /dev/null +++ b/src/Cfe/Parse/Base.agda @@ -0,0 +1,23 @@ +{-# OPTIONS --without-K --safe #-} + +open import Relation.Binary using (Setoid) + +module Cfe.Parse.Base + {c ℓ} (over : Setoid c ℓ) + where + +open Setoid over renaming (Carrier to C) + +open import Cfe.Expression over +open import Data.Fin +open import Data.List + +infix 4 _⤇_ + +data _⤇_ : Expression 0 → List C → Set c where + Eps : ε ⤇ [] + Char : ∀ {c} → Char c ⤇ [ c ] + Cat : ∀ {e₁ e₂ l₁ l₂} → e₁ ⤇ l₁ → e₂ ⤇ l₂ → e₁ ∙ e₂ ⤇ l₁ ++ l₂ + Veeˡ : ∀ {e₁ e₂ l} → e₁ ⤇ l → e₁ ∨ e₂ ⤇ l + Veeʳ : ∀ {e₁ e₂ l} → e₂ ⤇ l → e₁ ∨ e₂ ⤇ l + Fix : ∀ {e l} → e [ μ e / zero ] ⤇ l → μ e ⤇ l diff --git a/src/Cfe/Parse/Properties.agda b/src/Cfe/Parse/Properties.agda new file mode 100644 index 0000000..7803f82 --- /dev/null +++ b/src/Cfe/Parse/Properties.agda @@ -0,0 +1,7 @@ +{-# OPTIONS --without-K --safe #-} + +open import Relation.Binary using (Setoid) + +module Cfe.Parse.Properties + {c ℓ} (over : Setoid c ℓ) + where |