Zulip Chat Archive

Stream: lean4

Topic: unintended instance


Arthur Paulino (Nov 29 2021 at 00:37):

I'm trying to make Lean coerce 3.4 to Float but it seems like it's trying to coerce to OfScientific instead:

inductive Entry
  | str (s : String)
  | int (n : Int)
  | float (f : Float)
  | null

constant NULL : Entry := Entry.null

instance : Coe Int Entry where
  coe := Entry.int

instance : Coe String Entry where
  coe := Entry.str

instance : Coe Float Entry where
  coe := Entry.float

abbrev Row := List Entry

example : Row := [1, "e"] -- works
example : Row := [1, "e", 3.4] -- failed to synthesize instance OfScientific Entry

Any idea how to workaround this issue?


Last updated: Dec 20 2023 at 11:08 UTC