From d926ce9f2d1144f329598a30b3ed2e48899519b2 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Wed, 9 Oct 2024 16:57:47 +0100
Subject: Write a System T to Primrose program.

---
 program/syst-to-primrose.pty | 41 +++++++++++++++++++++++++++++++++++++++++
 1 file changed, 41 insertions(+)
 create mode 100644 program/syst-to-primrose.pty

(limited to 'program/syst-to-primrose.pty')

diff --git a/program/syst-to-primrose.pty b/program/syst-to-primrose.pty
new file mode 100644
index 0000000..4030642
--- /dev/null
+++ b/program/syst-to-primrose.pty
@@ -0,0 +1,41 @@
+(\X =>
+  [ Var: Nat
+  , Zero: <>
+  , Suc: X
+  , Rec: <Target: X, Zero: X, Suc: X>
+  , Abs: X
+  , App: <Fun: X, Arg: X>
+  ])
+->
+(\X =>
+  [ Var: Nat
+  , Lit: Nat
+  , Suc: X
+  , Abs: X
+  , App: <Fun: X, Arg: X>
+  , Unit: <>
+  , Pair: <Fst: X, Snd: X>
+  , Fst: X
+  , Snd: X
+  , Absurd: <Target: X>
+  , Inl: X
+  , Inr: X
+  , Case: <Target: X, Left: X, Right: X>
+  , Expand: X
+  , Contract: X
+  , Fold: <Target: X, Body: X>
+  , Let: <Bound: X, Body: X>
+  , Annot:
+    < Term: X
+    , Type: (\Y =>
+      [ Var: Nat
+      , N: <>
+      , Arrow: <Dom: Y, Cod: Y>
+      , Unit: <>
+      , Pair: <Fst: Y, Snd: Y>
+      , Bottom: <>
+      , Sum: <Left: Y, Right: Y>
+      , Fix: Y
+      ])
+    >
+  ])
-- 
cgit v1.2.3