[CakeML] Basis library

Lars Hupel hupel at in.tum.de
Thu Jul 20 13:38:18 UTC 2017


Hi Ramana,

> I put the result of running the following code at
> https://cakeml.org/basis-names.txt for now. (But don't expect that link to
> be kept up to date, or even alive.)

that's perfect! No need to keep it alive. I'm currently experimenting
with the bootstrapped snapshot you sent me in April (based on 32b749c3).

I'm mostly interested in string manipulation though, because in my work,
I need to print the result of my generated program. Otherwise, my
program would just "generate heat" and the user could not observe the
result. How do you deal with this in the HOL4 extraction? Can the user
say "generate me a program that computes `fib 5` and prints the result"?

Cheers
Lars



More information about the Users mailing list