Zulip Chat Archive

Stream: lean4

Topic: LCNF local context contains unused local variable declaratio


Marc Huisinga (Sep 27 2022 at 19:34):

MWE:

class NameableType (τ : Type) where
  name : String

instance : NameableType String where
  name := "String"

instance [inst : NameableType α] : NameableType (Array α) where
  name :=
    if inst.name.contains ' ' then
      s!"Array ({inst.name})"
    else
      s!"Array {inst.name}"

-- LCNF local context contains unused local variable declaration `_x.10`
def foo : String :=
  NameableType.name (Array String)

Leonardo de Moura (Sep 27 2022 at 23:54):

Fixed https://github.com/leanprover/lean4/commit/135790f41a4d937941acda0173760d2d70ca7d8a


Last updated: Dec 20 2023 at 11:08 UTC