program/reducer.pty


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17

Nat ->
data T
  [ Var: Nat
  ; Zero: <>
  ; Suc: T
  ; Primrec: <Zero: T; Suc: T; Target: T>
  ; Abs: T
  ; App: <Fun: T; Arg: T>
  ] ->
data T
  [ Var: Nat
  ; Zero: <>
  ; Suc: T
  ; Primrec: <Zero: T; Suc: T; Target: T>
  ; Abs: T
  ; App: <Fun: T; Arg: T>
  ]