stainless
stainless copied to clipboard
Inlining for genc
Tail recursive functions are easier to specify and verify in Stainless, which is why they are written so. Genc emits them as recursive functions. gcc can optimize them, but not all C compilers can. genc should possibly eliminate tail recursion itself.