Function decode_recursor_rule

crates/ffi/src/lean_env.rs:870–879

(
  obj: LeanBorrowed<'_>,
  cache: &mut Cache<'_>,
)

    5 => {
      let f = decode_expr(e.get_obj(0), cache);
      let a = decode_expr(e.get_obj(1), cache);
      Expr::app(f, a)
    },
    6 => {
      let binder_name = decode_name(e.get_obj(0), cache.global);
      let binder_typ = decode_expr(e.get_obj(1), cache);
      let body = decode_expr(e.get_obj(2), cache);
      let binder_info = decode_binder_info(e.get_num_8(0));
      Expr::lam(binder_name, binder_typ, body, binder_info)
    },
    7 => {
      let binder_name = decode_name(e.get_obj(0), cache.global);
      let binder_typ = decode_expr(e.get_obj(1), cache);