diff --git a/Language.agda b/Language.agda
new file mode 100644
index 0000000..21e0784
--- /dev/null
+++ b/Language.agda
@@ -0,0 +1,10 @@
+module Language where
+
+open import Data.String using (String)
+open import Data.Nat using (ℕ)
+
+data Expr : Set where
+    _+_ : Expr → Expr → Expr
+    _-_ : Expr → Expr → Expr
+    `_ : String → Expr
+    #_ : ℕ → Expr