Zygimantas Straznickas (Mar 15 2021 at 23:35):
-- Using List as carrier of `children`: works partial def recurseM [Monad μ] (curr: α) (action: α -> μ (List α)) : μ PUnit := do let children ← action curr children.forM (recurseM · action) def specificTraverseList : Option Unit := recurseM () (fun _ => some ) -- Using Array as carrier of `children`: partial def recurseM2 [Monad μ] (curr: α) (action: α -> μ (Array α)) : μ PUnit := do let children ← action curr children.forM (recurseM2 · action) -- When compiling definition below: -- `deep recursion was detected at 'replace' (potential solution: increase stack space in your system)` def specificTraverseArray : Option Unit := recurseM2 () (fun _ => some #)
Possibly a bug? I tried setting the thread stack size to huge values and it didn't help.
Leonardo de Moura (Mar 16 2021 at 02:19):
Pushed a fix https://github.com/leanprover/lean4/commits/master
Last updated: May 18 2021 at 23:14 UTC