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



Hi all,

Just out of curiosity, and because I guess this may be worth in some circumstances, I wonder if there exist some recommended ways to add custom obligations to Theory design and make them checked. I mean kind of style check and design rules check.

As an example, one may want to require all Theories to not contain any partial functions. Is there a way to do this without externally re-parsing and re-interpreting *.thy files? (which would be too error‑prone by the way). Do the Isabelle system have provision to invoke such a layer, feeding it with a structure corresponding to the Theory interpretation?

Hope my question is clear enough (I'm not sure). If not, just ask me to reword it.

With thanks

--
“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.