Zulip Chat Archive

Stream: lean4

Topic: strange printing of set_option in


view this post on Zulip Jason Gross (Mar 22 2021 at 18:36):

When I do set_option trace.Meta.synthInstance true in ..., is this supposed to get rid of character locations, as in


: failed to synthesize instance
  Arr (b ~> c) (Sort ?u.10588) 2

: [Meta.synthInstance] Arr (b ~> c) (Sort ?u.10588) 2 ==> Arr (b ~> c) (Sort ?u.10588) 2
  [Meta.synthInstance]

?


Last updated: May 18 2021 at 23:14 UTC