summaryrefslogtreecommitdiff
path: root/program/reducer.prim
diff options
context:
space:
mode:
Diffstat (limited to 'program/reducer.prim')
-rw-r--r--program/reducer.prim4
1 files changed, 2 insertions, 2 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 =