The Coq mailing list

[Benjamin Werner <werner>]

        Hi Freek,

I cannot think about something simillar having been carried out. My
guess would be that if anything has been done, then it would be in the
NuPRL team; they have thought a lot about reflection and I do not know
all their work. You may also fish some ideas looking at people having
worked on conditional rewriting, but I have absolutely no pointer on
the topic.

On the topic of a Field tactic, and more generaly about using
reflection for partial functions, there is certainly some interesting
work to be done. Using an inductive relation is interesting. I am
however not totaly sure it is necesary in your case. The division
function simply takes a third argument, namely a proof that the second
argument is not zero. My guess would be that the tactic then generates
this condition as a sub-goal ?
But provided you have added this condition as a hypothesis, I guess
you can use a traditional interpetation function ?

I write this without having thought much about it, so I certainly can
be wrong.



Cheers,


Benjamin