Zulip Chat Archive

Stream: general

Topic: Automatic ext lemmas fails when using parameters

Praneeth Kolichala (Jul 19 2022 at 19:09):

The following:

import tactic.ext

parameter (α : Type)

structure TestStruct :=
(x : α)


fails with the following error message:

injection tactic failed, argument must be an equality proof where lhs and rhs are of the form (c ...), where c is a constructor
α : Type,
x y : α,
 : {x := x} = {x := y}
 {x := x}.x = {x := y}.x

The example works if parameter is changed to variable. Why does this happen, and are there any workarounds?

Eric Wieser (Jul 19 2022 at 20:18):

The usual workaround is to not ever use parameter; we pretty much avoid it everywhere in mathlib

Last updated: Aug 03 2023 at 10:10 UTC