Translate Coq recursion that does not directly pattern matches

[pedrotst]

Cedille recursion is tied with recursion, which is not necessarily the case with Coq.
This brings us to the question of how to deal functions like f bellow.

Fixpoint f (x y : nat): nat :=
S ((fix g (a b: nat) := match a with
             | O => b
             | S a' => g a' b + f a' b
              end) x y).

[pedrotst]

A follow up question to this is how does coq figures out the decreasing argument here

[cwjnkins]

The following (somewhat involved) implementation of f in Cedille might provide at least some help in figuring out how to translate such examples: https://gist.github.com/cwjnkins/c0ca1553adaf0252494e9d36c117a7ed

The definition works like this: one must have f use pattern matching, and probably would require a local definition of g for each clause (or have this factored out). g must be given knowledge that, if its argument a is non-zero, then pred a has the type Type/f, by explicitly using the derived View family (for internalized typing derivations). That way, when you case-analyze a to get the predecessor a', you know that this has type Type/g for the first call and Type/f for the second call.