coercion

Stream: new members

[Calle Sönne]

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.

[Patrick Massot]

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

[Kenny Lau]

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 -/

[Calle Sönne]

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)),

[Kenny Lau]

the options are cumulative

[Kenny Lau]

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

[Calle Sönne]

oh

[Calle Sönne]

This is great, thanks :)