free variables in mk.injEq

Stream: lean4

[Scott Morrison]

Anyone see what is going on in:

-- (kernel) declaration has free variables 'O.mk.injEq'
structure O (c : False = False) where
  m : Prop

This came up in !4#3072

[Mario Carneiro]

A very strange workaround:

set_option genInjectivity false in
structure O (c : False = False) where
  m : Prop
gen_injective_theorems% O

[Scott Morrison]

Thanks! Reported as https://github.com/leanprover/lean4/issues/2188

[Kevin Buzzard]

Heh, presumably now the injectivity lemma is missing?

[Scott Morrison]

No, in Mario's suggestion there is a gen_injective_theorems% O command afterwards, which apparently successfully generates them! I