From f5b75edd91389f0a45045b707abfa36c746e8d54 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Thu, 30 Jan 2025 16:57:47 +0000
Subject: Modify definition of data types.

---
 program/reducer.prim | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'program/reducer.prim')

diff --git a/program/reducer.prim b/program/reducer.prim
index 3abbc97..af3abd5 100644
--- a/program/reducer.prim
+++ b/program/reducer.prim
@@ -1,14 +1,14 @@
 let Bool = [T: <>; F: <>] in
 let or (x : Bool) (y : Bool) : Bool = case x of {T u => T <>; F u => y} in
 let SysT =
-  (\T =>
+  data T
     [ Var: Nat
     ; Zero: <>
     ; Suc: T
     ; Primrec: <Zero: T; Suc: T; Target: T>
     ; Abs: T
     ; App: <Fun: T; Arg: T>
-    ])
+    ]
 in
 let Stepped = <Term: SysT; Smaller: Bool> in
 let lift (f : Nat -> Nat) (n : Nat) : Nat =
-- 
cgit v1.2.3