Paolo Giarrusso (Dec 02 2020 at 15:01): Paolo Giarrusso (Dec 02 2020 at 15:01):Sometimes I want Context to use generalization, without re-generalizing on already available assumptions
Paolo Giarrusso (Dec 02 2020 at 15:01):Is this a sensible feature request?
Paolo Giarrusso (Dec 02 2020 at 15:02):(I can provide an example in a moment)
Paolo Giarrusso (Dec 02 2020 at 15:54):Haven't minimized properly, but sometimes in cases like
Class A1 := {}.
Class A2 := {}.
Class B `{A1}:= {}.
Class C `{A1} `{A2} := {}.
Section test.
Context `{!A1} `{!B} `{C}.
End test.
you see that `{!C} would fail (correctly) but `{C} abstracts over a separate A1 instance :-( (not sure if the above is enough to trigger it).
Gaëtan Gilbert (Dec 02 2020 at 16:09):i think ! uses tc inference, but generalization comes before tc inference
I guess you have to be explicit:
Generalizable All Variables.
Context `{!A1} `{!B} `{@C _ xbar}.
Last updated: Oct 13 2024 at 01:02 UTC