Code generator support for recursors

[eric-wieser]

Prerequisites

• [X] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

I couldn't see a tracking issue for this, so thought I'd create one to refer to from mathlib4. We quite often use Nat.rec and List.rec, and neither are supported by the code generator:

https://github.com/leanprover/lean4/blob/a125a36bcc79a28963ed5786f94c5d97648a8f99/src/Lean/CoreM.lean#L280-L295

Steps to Reproduce

Run

#eval (List.rec 0 (fun x xs ih => 0) ([] : List Nat) : Nat)

Expected behavior: Prints 0

Actual behavior:

code generator does not support recursor 'List.rec' yet, consider using 'match ... with' and/or structural recursion

Reproduces how often: 100%

[gebner]

See also the discussion at https://github.com/leanprover/std4/pull/91