Extracting a subexpression to an auxiliary declaration

Stream: lean4

[Eric Wieser]

Is there some outline elaborator, or a function in Lean.Elab, that can be used to make

def foo (a b c) := a + outline(b + c)

elaborate as

mutual
def foo.aux1 (b c) := b + c

def foo (a b c) := a + foo.aux1 b c
end

[Notification Bot]

This topic was moved here from #Is there code for X? > Extracting a subexpression to an auxiliary declaration by Eric Wieser.