This PR adds support for basic recursive functions. Mutually recursive functions are not supported yet. We use Meta.getUnfoldEqnFor? instead of Meta.unfoldDefinition? because the latter returns the kernel's definition of functions. Since the kernel does not support recursive functions, unfoldDefinition? returns their definition in terms of general recursors and WellFounded.fix. It's hard to recover the original definition from those compiled versions, so we use Meta.getUnfoldEqnFor? to get the user friendly version shown by the unfold tactic.
This PR adds support for basic recursive functions. Mutually recursive functions are not supported yet. We use
Meta.getUnfoldEqnFor?instead ofMeta.unfoldDefinition?because the latter returns the kernel's definition of functions. Since the kernel does not support recursive functions,unfoldDefinition?returns their definition in terms of general recursors andWellFounded.fix. It's hard to recover the original definition from those compiled versions, so we useMeta.getUnfoldEqnFor?to get the user friendly version shown by theunfoldtactic.