For those interested in these things; the discussion (lifted from a
series of posts to Qilang) is on http://www.lambdassociates.org/Lib/Logic/Martin-Lof/martin-lof.pdf.
It covers Per Martin-Lof's TT0 up to primitive recursion and includes
the synthesis of the addition function as an example (cor, wow ;)).
The code for the system is in http://www.lambdassociates.org/Lib/libraries.htm;
about 200 lines in all.
Mark