Stream: Coq users

Topic: Usable Context ` without !


view this post on Zulip Paolo Giarrusso (Dec 02 2020 at 15:01):

Sometimes I want Context to use generalization, without re-generalizing on already available assumptions

view this post on Zulip Paolo Giarrusso (Dec 02 2020 at 15:01):

Is this a sensible feature request?

view this post on Zulip Paolo Giarrusso (Dec 02 2020 at 15:02):

(I can provide an example in a moment)

view this post on Zulip 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).

view this post on Zulip 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: Jan 29 2023 at 01:02 UTC