Lean4
/-- Return the consecutive unfoldings of `e`. -/
partial def unfolds (e : Expr) : MetaM (Array Expr) := do
let e' ← whnfCore e
go e' (if e == e' then #[] else #[e'])
where/-- Append the unfoldings of `e` to `acc`. Assume `e` is in `whnfCore` form. -/
go (e : Expr) (acc : Array Expr) : MetaM (Array Expr) :=
tryCatchRuntimeEx
(withIncRecDepth
(do
if let some e := e.etaExpandedStrict? then
let e ← whnfCore e
return ← go e (acc.push e)
if let some e← reduceNat? e then
return acc.push e
if let some e← reduceNative? e then
return acc.push e
if let some e← unfoldProjDefaultInst? e then
-- when unfolding a default instance, don't add it to the array of unfolds.
let e ← whnfCore e
return ← go e acc
if let some e← unfoldDefinition? e then
-- Note: whnfCore can give a recursion depth error
let e ← whnfCore e
return ← go e (acc.push e)
return acc))
fun _ => return acc
