Skip to content

mlRewriteBy fails if goal matches LHS of =ml #448

@Thrithralas

Description

@Thrithralas

The following mlRewriteBy fails:

Example wrong {Σ : Signature}{syntax : Syntax}(Γ : Theory) (a b : Pattern) :
    theory ⊆ Γ ->
    well_formed a = true ->
    well_formed b = true ->
    Γ ⊢ a =ml b ---> b ---> a.
Proof.
  intros.
  mlIntro. mlIntro.
  Fail mlRewriteBy "0" at 1.
Abort.

The expected outcome should be, that the goal gets rewritten from a to b, however it fails with the following error:

Unable to unify "?goal@{a:={| pcEvar := star; pcPattern := patt_free_evar star |} [a]}"
with "{| pcEvar := star; pcPattern := patt_free_evar star |} [a]"
(cannot instantiate "?goal" because "a" is not in its scope: available arguments are 
"Σ" "syntax" "Γ" "{| pcEvar := star; pcPattern := patt_free_evar star |} [a]" 
"b" "H" "H0" "H1" "star" "star_eq" "heq1").

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions