Re: [isabelle] Encoding an evaluation context



Alternatively you can encode the evaluation contexts as congruence rules: for
each pattern in the context grammar you define a rule

xi -> xi'
-----------------------------
c x1 ... xn -> c x1 .. xi' xn

This is very straightforward but does not please friends of  eval-contexts.

Tobias





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.