mathlib

mathlib copied to clipboard

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