Re: [isabelle] What is sumC?



> I searched the code generation manual for code-simp and eval. Code-simp
> appears in only one place in that manual, and it's in the Schematic
> Diagram (section 6.3), which hardly qualifies as a description.

It's slightly more detailed in §6.1.

> Having said this, though, it doesn't look as if I'll be able to use
> these, anyway. The Abstract to the code generation manual says that "the
> code generator facilities of Isabelle/HOL...empower the user to turn HOL
> specifications into corresponding executable programs in the languages
> SML, OCaml, Haskell and Scala." I'm based in the US, and my only
> exposure to functional languages has been to Lisp. (Maybe that's
> chauvinistic, since Lisp was developed in the US.) I've been studying
> Paulson's ML book, but I haven't actually used ML yet.

The 'code_simp' and 'eval' methods are using code generator
infrastructure, but are not actually generating code (at least not
observably). They are completely embedded in Isabelle and have nothing
to do with any of the targets the code generator supports.

Cheers
Lars




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.