program/reducer.pty


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
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>
  ])