Explanation for recursor?

Stream: lean4

[Siddharth Bhat]

How do I perform mutual induction in LEAN4? I believe that this is not implemented yet, so I'm trying to use elimination principles to write my mutual induction by hand. Consider:

mutual
  inductive Expr
  | expr_int: Int -> Expr
  | expr_neg: Expr -> Expr
inductive Block
  | block_empty: Block
  end
open Expr

Asking Lean with #check Expr.brec_on and #check Expr.below gives:

Expr.below : Expr → Sort (max 1 u_1)
Expr.brecOn : (t : Expr) → ((t : Expr) → Expr.below t → ?m.398 t) → ((t : Block) → Block.below t → ?m.399 t) → ?m.398 t

Where can I read more about Expr.below and how to use it? The docs about inductive types say:

Lean also generates the predicate transformer below and the recursor brec_on. It is unlikely that you will ever need to use these constructions directly; they are auxiliary definitions used by the recursive equation compiler we will describe in the next chapter, and we will not discuss them further here.

What I actually want to do is to have an induction principle like:

def induction_expr:
  (mot_expr: Expr -> Prop)
  (mot_block: Block -> Prop)
  -- EXPR
  (base_expr_int: forall (i: Int), mot_expr (expr_int i))
  (ind_expr_neg: forall (e: Expr)
    (MOT_NEG: mot_expr e), mot_expr (expr_neg e)):
  -- FINAL
    forall (e: Expr), mot_expr e :=

or some such.

[Sebastian Ullrich]

Mutual recursion has been implemented: https://github.com/leanprover/lean4/blob/master/tests/lean/run/mutwf2.lean