Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

nth_rewrite incorrectly unifies universe variables #14994

Open
fpvandoorn opened this issue Jun 27, 2022 · 0 comments
Open

nth_rewrite incorrectly unifies universe variables #14994

fpvandoorn opened this issue Jun 27, 2022 · 0 comments
Labels
bug t-meta Tactics, attributes or user commands

Comments

@fpvandoorn
Copy link
Member

In the following example, nth_rewrite incorrectly instantiates the universe metavariable of h with 0, but still rewrites with the hypothesis. Note that rw does this correctly.

def foo (h : ∀ {α : Type*} (x : α), id x = x) : id tt = tt :=
begin
  nth_rewrite 0 [h], -- error in resulting proof term
  -- rw [h], -- works
end
@fpvandoorn fpvandoorn added bug t-meta Tactics, attributes or user commands labels Jun 27, 2022
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
bug t-meta Tactics, attributes or user commands
Projects
None yet
Development

No branches or pull requests

1 participant