[isabelle] Ways to add a checking layer for Theories?
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
“Syntactic sugar causes cancer of the semi-colons.” 
“Structured Programming supports the law of the excluded muddle.” 
: Epigrams on Programming — Alan J. — P. Yale University
This archive was generated by a fusion of
Pipermail (Mailman edition) and