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.

Are you looking for something like mutual recursion in https://isabelle.in.tum.de/doc/functions.pdf (Section 5)?

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

Thanks, makes perfect sense :-)

Last updated: Sep 25 2021 at 09:17 UTC