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.


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