diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2024-10-29 18:58:45 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2024-10-29 18:58:45 +0000 |
| commit | 82783476f330801b54402bdcc4723add44a963dc (patch) | |
| tree | a1f8e77bf4a8fa32bb52e4e26c06f8acbb136df9 /program/reducer.pty | |
| parent | 324e22d7297f506f7ba551f0d1e9aac786ae4622 (diff) | |
Write a fuelled reducer for System T.
Diffstat (limited to 'program/reducer.pty')
| -rw-r--r-- | program/reducer.pty | 17 |
1 files changed, 17 insertions, 0 deletions
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> + ]) |