lambda body

Stream: Is there code for X?

[Aaron Liu]

Like docs#Lean.Expr.getForallBody but for lambda expressions (I'm not in MetaM)

[Eric Wieser]

if let .lam _ _ _ _ := e then _ else _?

[Edward van de Meent]

i have noticed that a bunch of these meta functions only have forall and let versions, but never lambda...

[Edward van de Meent]

depending on your usecase, there can be different ways around this.

[Aaron Liu]

Eric Wieser said:

if let .lam _ _ _ _ := e then _ else _?

If you have a fun a b => body this gives fun b => body but I want body

[Kyle Miller]

I think there used to be a function like that hanging around in Lean.Elab.Structure/StructInst, but it got refactored away. It's easy enough to make a custom one for your own metaprogram.

(Can I ask what you're wanting this for?)

[Kyle Miller]

Oh right, I saw another copy of this function recently, docs#Lean.Meta.AbstractNestedProofs.getLambdaBody

[Kyle Miller]

I'd imagine a PR moving this function into Lean.Expr wouldn't be unwelcome.