From 82783476f330801b54402bdcc4723add44a963dc Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Tue, 29 Oct 2024 18:58:45 +0000
Subject: Write a fuelled reducer for System T.

---
 program/reducer.pty | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 program/reducer.pty

(limited to 'program/reducer.pty')

diff --git a/program/reducer.pty b/program/reducer.pty
new file mode 100644
index 0000000..996541b
--- /dev/null
+++ b/program/reducer.pty
@@ -0,0 +1,17 @@
+Nat ->
+(\T =>
+  [ Var: Nat
+  , Zero: <>
+  , Suc: T
+  , Primrec: <Zero: T, Suc: T, Target: T>
+  , Abs: T
+  , App: <Fun: T, Arg: T>
+  ]) ->
+(\T =>
+  [ Var: Nat
+  , Zero: <>
+  , Suc: T
+  , Primrec: <Zero: T, Suc: T, Target: T>
+  , Abs: T
+  , App: <Fun: T, Arg: T>
+  ])
-- 
cgit v1.2.3