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 ++--
 program/reducer.pty  | 8 ++++----
 2 files changed, 6 insertions(+), 6 deletions(-)

(limited to 'program')

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 =
diff --git a/program/reducer.pty b/program/reducer.pty
index c72b8c6..65090e5 100644
--- a/program/reducer.pty
+++ b/program/reducer.pty
@@ -1,17 +1,17 @@
 Nat ->
-(\T =>
+data T
   [ Var: Nat
   ; Zero: <>
   ; Suc: T
   ; Primrec: <Zero: T; Suc: T; Target: T>
   ; Abs: T
   ; App: <Fun: T; Arg: T>
-  ]) ->
-(\T =>
+  ] ->
+data T
   [ Var: Nat
   ; Zero: <>
   ; Suc: T
   ; Primrec: <Zero: T; Suc: T; Target: T>
   ; Abs: T
   ; App: <Fun: T; Arg: T>
-  ])
+  ]
-- 
cgit v1.2.3