summaryrefslogtreecommitdiff
path: root/program/syst-to-primrose.pty
diff options
context:
space:
mode:
Diffstat (limited to 'program/syst-to-primrose.pty')
-rw-r--r--program/syst-to-primrose.pty41
1 files changed, 0 insertions, 41 deletions
diff --git a/program/syst-to-primrose.pty b/program/syst-to-primrose.pty
deleted file mode 100644
index 4030642..0000000
--- a/program/syst-to-primrose.pty
+++ /dev/null
@@ -1,41 +0,0 @@
-(\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
- ])
- >
- ])