From 8dc5c40eae16befc3c9fd6af2ea752ff3415dfdb Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sat, 13 Apr 2024 14:13:44 -0700
Subject: [PATCH] Get everything compiling

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 Language.agda |  1 +
 Main.agda     | 14 ++++++--------
 2 files changed, 7 insertions(+), 8 deletions(-)

diff --git a/Language.agda b/Language.agda
index d6aa45c..d6f83f0 100644
--- a/Language.agda
+++ b/Language.agda
@@ -37,6 +37,7 @@ data BasicStmt : Set where
     _←_ : String → Expr → BasicStmt
     noop : BasicStmt
 
+infixr 2 _then_
 data Stmt : Set where
     ⟨_⟩ : BasicStmt → Stmt
     _then_ : Stmt → Stmt → Stmt
diff --git a/Main.agda b/Main.agda
index 176bd5f..09ad11d 100644
--- a/Main.agda
+++ b/Main.agda
@@ -6,18 +6,16 @@ open import Data.Vec using (Vec; _∷_; [])
 open import IO
 open import Level using (0ℓ)
 
-testCode : Vec Stmt _
+testCode : Stmt
 testCode =
-    ("zero" ← (# 0)) ∷
-    ("pos" ← ((` "zero") Expr.+ (# 1))) ∷
-    ("neg" ← ((` "zero") Expr.- (# 1))) ∷
-    ("unknown" ← ((` "pos") Expr.+ (` "neg"))) ∷
-    []
+    ⟨ "zero" ← (# 0) ⟩ then
+    ⟨ "pos" ← ((` "zero") Expr.+ (# 1)) ⟩ then
+    ⟨ "neg" ← ((` "zero") Expr.- (# 1)) ⟩ then
+    ⟨ "unknown" ← ((` "pos") Expr.+ (` "neg")) ⟩
 
 testProgram : Program
 testProgram = record
-    { length = _
-    ; stmts = testCode
+    { rootStmt = testCode
     }
 
 open WithProg testProgram using (output)