Re: [isabelle] Ways to add a checking layer for Theories?



On 04.08.2012 13:46, Yannick Duchêne (Hibou57) wrote:
I'll do the easy part and point out page 14 of prog-prove.pdf:

"...all HOL functions must be total. This simplifies the logic—terms
are always defined—but means that recursive functions must terminate."

You probably have other examples in mind, and maybe you're not using HOL.

Not that much, I “imports Main”, and that way it's easy to have a “fun”
which does not cover all cases, with no error and just a warning.

These functions are nevertheless total; you just don't know anything about the values for the uncovered case.

  -- Lars





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