Den 2017-12-02 kl. 21:56, skrev Joachim Breitner:
With a wee bit of higher-order matching, one might make `u` and `v`
functions and instead write:
foo (\ x -> fmap (u x) (v x)) = bar u v
In that case I'd expect `u` and `v` to be synthesized rather than
literally matched. For instance, `foo
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
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. ...
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
