diff options
author | Greg Brown <greg.brown01@ed.ac.uk> | 2025-01-07 13:50:13 +0000 |
---|---|---|
committer | Greg Brown <greg.brown01@ed.ac.uk> | 2025-01-07 13:50:13 +0000 |
commit | f2490f5ca35b528c7332791c6932045eb9d5438b (patch) | |
tree | 9a4caa4715705dcc4965d4507213ce4ca29e0add /program/reducer.pty | |
parent | 0ecd9e608ced18f70f465c986d6519e8e95b0b6b (diff) |
Add quotation to help metaprogramming.
Diffstat (limited to 'program/reducer.pty')
-rw-r--r-- | program/reducer.pty | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/program/reducer.pty b/program/reducer.pty index 996541b..c72b8c6 100644 --- a/program/reducer.pty +++ b/program/reducer.pty @@ -1,17 +1,17 @@ Nat -> (\T => [ Var: Nat - , Zero: <> - , Suc: T - , Primrec: <Zero: T, Suc: T, Target: T> - , Abs: T - , App: <Fun: T, Arg: T> + ; 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> + ; Zero: <> + ; Suc: T + ; Primrec: <Zero: T; Suc: T; Target: T> + ; Abs: T + ; App: <Fun: T; Arg: T> ]) |