Robert Soeldner (May 28 2021 at 10:59): Robert Soeldner (May 28 2021 at 10:59):Is it possible to forward declare function? I want to implement def. 46, Page 50 https://arxiv.org/pdf/2010.14549.pdf in which the construction of Success depends on Pre and vice versa.
Mathias Fleury (May 28 2021 at 11:01):Are you looking for something like mutual recursion in https://isabelle.in.tum.de/doc/functions.pdf (Section 5)?
Mathias Fleury (May 28 2021 at 11:01):Forward declaration is not possible because you need the definition to prove termination
Robert Soeldner (May 28 2021 at 11:02):Thanks, makes perfect sense :-)
Last updated: Apr 24 2024 at 20:16 UTC