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.
Phil
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.
Regards,
Rob.
------------------------------------------------------------------------
_______________________________________________
Proofpower mailing list
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
_______________________________________________
Proofpower mailing list
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
