Hi,
Am Samstag, den 02.12.2017, 12:59 -0800 schrieb Conal Elliott:
> Thanks for the reply, Ed.
>
> > I'd assume that `x` didn't occur in either `u` or `v`
>
> This is exactly the issue I'm wondering about. Since rewrite rules
> admit lambdas and only first-order matching, I'm wondering whether
>
Thanks for the reply, Ed.
> I'd assume that `x` didn't occur in either `u` or `v`
This is exactly the issue I'm wondering about. Since rewrite rules admit
lambdas and only first-order matching, I'm wondering whether they're
interpreted as you did (and I'd tend to), namely that `x` doesn't occur
f
I don't knw of a formal writeup anywhere.
But does that actually mean what you are trying to write?
With the effective placement of "forall" quantifiers on the outside for u
and v I'd assume that x didn't occur in either u or v. Effectively you have
some scope like forall u v. exists x. ...
Unde
Is there a written explanation and/or examples of rewrite rules involving a
LHS lambda? Since rule matching is first-order, I'm wondering how terms
with lambda are matched on the LHS and substituted into on the RHS. For
instance, I want to restructure a lambda term as follows:
> foo (\ x -> fmap u
