\v0 -> v0 1



? 1



? 1



unknown variable unknown_var

unknown variable unknown_var

literal of function type

f 1 2



\v0 -> v0



?666



f



f 1 2



literal of function type

2



g 0



\v0 -> g v0



g ?



5



3



g2



f 3.2



g2 2.3



g2 (f 0) 1



3.14



succ zero



?



\v0 -> dec v0



dec ?



g3 ? 0



g (g2 ? 0)



succ (succ zero)



zero



succ err