pretty printing `Rat`

Stream: lean4

[Kyle Miller]

@Yaël Dillies You mentioned you have pretty printing issues with Rat. You you give an example?

[Yaël Dillies]

I am currently working on defining NNRat.cast in #11203 and as such I need to understand proofs like the one of docs#Rat.cast_mk_of_ne_zero. In there, you see a goal of ⊢ ↑{ num := n, den := d, den_nz := h, reduced := c } = ↑a / ↑b (at the -- Porting note: was symm) and the corresponding goal in the NNRat version (which is in #11203 but not master) is even worse because there an extra Subtype.mk on top.

[Eric Wieser]

I'm not sure I understand what you expect it to print as

[Yaël Dillies]

Anything less verbose. ⟨n, d, h, c⟩ would be great (maybe not as the default but at least as a set_option)

[Eric Rodriguez]

There is a set option for this, pp.structureInstances or something of the like iirc