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