diff options
Diffstat (limited to 'program')
| -rw-r--r-- | program/reducer.prim | 4 | ||||
| -rw-r--r-- | program/reducer.pty | 8 |
2 files changed, 6 insertions, 6 deletions
diff --git a/program/reducer.prim b/program/reducer.prim index 3abbc97..af3abd5 100644 --- a/program/reducer.prim +++ b/program/reducer.prim @@ -1,14 +1,14 @@ let Bool = [T: <>; F: <>] in let or (x : Bool) (y : Bool) : Bool = case x of {T u => T <>; F u => y} in let SysT = - (\T => + data T [ Var: Nat ; Zero: <> ; Suc: T ; Primrec: <Zero: T; Suc: T; Target: T> ; Abs: T ; App: <Fun: T; Arg: T> - ]) + ] in let Stepped = <Term: SysT; Smaller: Bool> in let lift (f : Nat -> Nat) (n : Nat) : Nat = diff --git a/program/reducer.pty b/program/reducer.pty index c72b8c6..65090e5 100644 --- a/program/reducer.pty +++ b/program/reducer.pty @@ -1,17 +1,17 @@ Nat -> -(\T => +data T [ Var: Nat ; Zero: <> ; Suc: T ; Primrec: <Zero: T; Suc: T; Target: T> ; Abs: T ; App: <Fun: T; Arg: T> - ]) -> -(\T => + ] -> +data T [ Var: Nat ; Zero: <> ; Suc: T ; Primrec: <Zero: T; Suc: T; Target: T> ; Abs: T ; App: <Fun: T; Arg: T> - ]) + ] |