This sounds very useful - only today I was having to introduce lambda terms for rewriting to match with... but in Z, not HOL. Will these higher-order matching/rewriting facilities be implemented for Z also? If not, does the updated rewriting infrastructure support a corresponding implementation for ProofPower-Z?

I can see Z has complications for lambda abstractions not over U but expecting the domain condition as per z_%beta%_conv seems ok.


Rob Arthan wrote:
Dear All,

I am looking at higher-order rewriting. The cleanest way to implement it will involve adding an extra parameter to the functions prim_rewrite_conv, prim_rewrite_rule and prim_rewrite_tac (which I suspect aren't very widely used). The parameter value will be optional and supplying Nil will give the same behaviour as currently. If anybody has code that would be badly affected by this, please let me know.




Proofpower mailing list

Proofpower mailing list

Reply via email to