Stream: Beginner Questions

Topic: Forward declaration


view this post on Zulip 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.

view this post on Zulip 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)?

view this post on Zulip Mathias Fleury (May 28 2021 at 11:01):

Forward declaration is not possible because you need the definition to prove termination

view this post on Zulip Robert Soeldner (May 28 2021 at 11:02):

Thanks, makes perfect sense :-)


Last updated: Sep 25 2021 at 09:17 UTC