[isabelle] Where to learn about the Mini-Haskell of the code generator?

Hi people,

The codegen.pdf document, says a single translations occurs before serialization to a target language. This prior translation is said to have a single target of its own: a kind of Mini-Haskell.

Is this Mini-Haskell described in some official or unofficial documents? (I don't know Haskell, just SML)

By the way, why a Mini-Haskell instead of a Mini-SML? What do Haskell offers here SML can't for this purpose? (not a criticism, that's just to learn the rational behind it).

Have an happy day

“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

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