agda2scheme
agda2scheme copied to clipboard
Published
20 hours ago •
jespercockx
jespercockx
Compile nat-like and int-like types to integers
It would be cool if we could detect automatically types that are sufficiently like natural numbers or integers, and represent them using actual integers in the compiled code. As a stretch goal, we could even try to detect that certain functions are just addition/subtraction/... and compile them to more efficient versions as well.
