10
10
let plus = << fun n -> fun m -> $rec_nat$ n (fun n -> fun p -> $succ$ p) m >>
11
11
let times = << fun n -> fun m -> $rec_nat$ n (fun n -> fun p -> $plus$ m p) $zero$ >>
12
12
let fact = << fun n -> $rec_nat$ n (fun n -> fun p -> $times$ ($succ$ n) p) $one$ >>