Define expressions

2 files changed, 23 insertions, 0 deletions

diff --git a/src/Cfe/Expression.agda b/src/Cfe/Expression.agda
new file mode 100644
index 0000000..e264926
--- /dev/null
+++ b/src/Cfe/Expression.agda
@@ -0,0 +1,7 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Cfe.Expression
+  {ℓ} (A : Set ℓ)
+  where
+
+open import Cfe.Expression.Base A public
diff --git a/src/Cfe/Expression/Base.agda b/src/Cfe/Expression/Base.agda
new file mode 100644
index 0000000..3545f9a
--- /dev/null
+++ b/src/Cfe/Expression/Base.agda
@@ -0,0 +1,16 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Cfe.Expression.Base
+  {ℓ} (A : Set ℓ)
+  where
+
+open import Data.Nat
+
+data Expression : ℕ → Set ℓ where
+  ⊥ : {n : ℕ} → Expression n
+  ε : {n : ℕ} → Expression n
+  Char : {n : ℕ} → A → Expression n
+  _∨_ : {n : ℕ} → Expression n → Expression n → Expression n
+  _∙_ : {n : ℕ} → Expression n → Expression n → Expression n
+  Var : {m : ℕ} → (n : ℕ) → Expression (suc (m + n))
+  μ : {n : ℕ} → Expression (suc n) → Expression n