a706c3b89a
When projection functions are delaborated, intermediate parent projections are no longer printed. For example, rather than pretty printing as `o.toB.toA.x` with these `toB` and `toA` parent projections, it pretty prints as `o.x`. This feature is being upstreamed from mathlib.
12 lines
372 B
Text
12 lines
372 B
Text
def foo : A → B → B :=
|
|
fun a b => { x := a.x, y := b.y }
|
|
def boo : A → B → B :=
|
|
fun a b => { x := b.x, y := b.y }
|
|
def baz : A → B → C :=
|
|
fun a b => { toB := { x := a.x, y := b.y } }
|
|
def biz : A → B → C :=
|
|
fun a b => { toB := b }
|
|
def faz : A → C → C :=
|
|
fun a c => { toB := { x := a.x, y := c.y } }
|
|
def fiz : A → C → C :=
|
|
fun a c => { toB := c.toB }
|