Metafunctions in O position of Judgment Not Working about redex HOT 7 CLOSED

from redex.

I believe he's saying it is broken

Jay

On Friday, September 25, 2015, Robby Findler [email protected]
wrote:

The O positions are syntactically restricted to be patterns (inside
judgment forms anyway) and metafunctions can go in patterns. Are you
suggesting a different rule? (Can you say what the rule would be?)

—
Reply to this email directly or view it on GitHub
#13 (comment).

Jay McCarthy
http://jeapostrophe.github.io

       "Wherefore, be not weary in well-doing,
  for ye are laying the foundation of a great work.

And out of small things proceedeth that which is great."
- D&C 64:33

from redex.

The metafunction top2 should evaluate to top which in the 2nd to last example above, but it doesn't.

from redex.

On Fri, Sep 25, 2015 at 3:20 PM, Max S. New [email protected]
wrote:

The metafunction top2 should evaluate to top which in the 2nd to last
example above, but it doesn't.

I don't see why you think that. Metafunctions aren't allowed to be used in
patterns. Maybe you're missing the syntax error message? Or maybe you're
thinking of some change to the semantics of Redex that makes it make sense
to put metafunctions in patterns somehow?

Robby

from redex.

Oh above you said metafunctions "can" go into patterns but I see now you meant "can't".

So I guess I'm proposing that in a pattern a metafunction is just evaluated and its output used as a pattern.

from redex.

from redex.

Well, this seems to be a big semantics discussion we could have and so probably best not to do that in a github issue, so I'm closing this. If it seems wrong to you, please reopen.

from redex.