Function decode_constant_val

crates/ffi/src/lean_env.rs:881–893

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

    },
    7 => {
      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::all(binder_name, binder_typ, body, binder_info)
    },
    8 => {
      let decl_name = decode_name(e.get_obj(0), cache.global);
      let typ = decode_expr(e.get_obj(1), cache);
      let value = decode_expr(e.get_obj(2), cache);
      let body = decode_expr(e.get_obj(3), cache);
      let nondep = e.get_num_8(0) != 0;
      Expr::letE(decl_name, typ, value, body, nondep)
    },
    9 => {
      let lit = LeanIxLiteral::from_ctor(e.get_obj(0).as_ctor());