Commit 5818378d authored by's avatar

RAE's response to SPJ's question in flattening-notes

parent ac73d1a7
......@@ -225,3 +225,8 @@ rewrite
Well, it depends on the roles at which T uses its arguments :-(.
So it may not be enough just to look at (flavour,role) pairs?
RAE: This is true, but it is taken care of by being careful in the
flattening algorithm. Flattening (T a) looks at the roles of
T's parameters, and chooses the role for flattening `a` appropriately.
This is why there must be the [Role] parameter to flattenMany.
Of course, this non-uniform rewriting may gum up the proof works.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment