Zulip Chat Archive

Stream: new members

Topic: coercion


view this post on Zulip Calle Sönne (Feb 25 2019 at 19:27):

Is there anyway to make lean display what type of coercion it is in the parser? Right now I'm working on a problem where there are coercions from int to the ring, from nat to the ring and from nat to int to the ring. It gets quite confusing when everything is displayed with jus \u.

view this post on Zulip Patrick Massot (Feb 25 2019 at 19:29):

set_option pp.all true certainly does the job, but there may be less radical options

view this post on Zulip Kenny Lau (Feb 25 2019 at 19:29):

set_option pp.notation false

#check ((2:):) -- coe 2 : int

set_option pp.implicit true

#check ((2:):) -- @coe nat int (@coe_to_lift nat int (@coe_base nat int int.has_coe)) 2 : int

set_option pp.all true

#check ((2:):)
/- @coe.{1 1} nat int (@coe_to_lift.{1 1} nat int (@coe_base.{1 1} nat int int.has_coe))
  (@bit0.{0} nat nat.has_add (@has_one.one.{0} nat nat.has_one)) :
  int -/

view this post on Zulip Calle Sönne (Feb 25 2019 at 19:38):

pp.imlicit true seems to expand most things except coercions for me:

@fract α _inst_1 _inst_2 r * b ^ nat.succ n * b =
    @finset.sum   (@semiring.to_add_comm_monoid  int.semiring) (finset.range (nat.succ n))
      (λ (x : ), @digit α _inst_1 _inst_2 b r x * b ^ (nat.succ n - 1 - x + 1)),

view this post on Zulip Kenny Lau (Feb 25 2019 at 19:39):

the options are cumulative

view this post on Zulip Kenny Lau (Feb 25 2019 at 19:39):

in particular, the second one is the result of both pp.notation false and pp.implicit true

view this post on Zulip Calle Sönne (Feb 25 2019 at 19:39):

oh

view this post on Zulip Calle Sönne (Feb 25 2019 at 19:40):

This is great, thanks :)


Last updated: May 16 2021 at 05:21 UTC