pp.analyze not working

Stream: general

[Frederick Pu]

I'm trying to get pretty printed type annotations but it's not working

open Lean

set_option pp.analyze true
set_option pp.analyze.checkInstances true
set_option pp.analyze.typeAscriptions true


#check ((1 : Nat) : Int)
-- ↑1 : Int

[Aaron Liu]

Try set_option pp.numericTypes true and set_option pp.coercions.types true

[Frederick Pu]

thx works now:

open Lean

-- set_option pp.analyze true
-- set_option pp.analyze.checkInstances true
-- set_option pp.analyze.typeAscriptions true
set_option pp.coercions.types true
set_option pp.numericTypes true

#check ((1 : Nat) : Int)
-- (↑(1 : Nat) : Int) : Int