Skip to content
  • Tej Chajed's avatar
    Use user names when destructing existentials · 7d0bb151
    Tej Chajed authored and Robbert Krebbers's avatar Robbert Krebbers committed
    When running `iDestruct "H" as (?) "H"`, use the name of the binder in
    "H". For example, if "H" has type `∃ y, Φ y`,  we now use `y` as the
    name of the variable after freshening. Previously the name was always
    the equivalent of running `fresh H`.
    The implementation achieves this by forwarding the desired identifier
    name through the `IntoExist` typeclass. Identifiers are serialized in
    Gallina by using them as the name of a function of type `ident_name :=
    unit -> unit`.