The Coq mailing list

[Freek Wiedijk <freek AT cs.kun.nl>]

Hi,

I have a question.  I'm contemplating doing "partial
reflection".  By this I mean "reflexion" (the "two-level
approach") but with "undefined expressions" on the
syntactical level.  My idea is to replace the "interpretation
function" by an inductively generated "interpretation
relation" to model a partial & multi-valued function.

In that way one can have expressions like "1/0" on the
syntactical level, without the need to be able to "evaluate"
it to some real number on the semantical level.

I want something like that, because I want to generalize the
"Ring" tactic of Coq to include division too (so to generalize
it to a "Field" tactic.)

I wonder: has anything like this be done already?  If so:
can anyone give me pointers to something about it in the
literature or on the web?

Freek