Method all_mdata_with_addr

crates/kernel/src/expr.rs:479–495

(
    name: M::MField<Name>,
    bi: M::MField<BinderInfo>,
    ty: KExpr<M>,
    body: KExpr<M>,
    mdata: M::MField<Vec<MData>>,
    addr: Addr,
  )

      ty.lbr().max(body.lbr().saturating_sub(1)),
      ty.count_0(),
      ty.has_fvars() || body.has_fvars(),
      mdata,
    );
    KExpr::new(ExprData::All(name, bi, ty, body, info))
  }

  pub fn all_mdata(
    name: M::MField<Name>,
    bi: M::MField<BinderInfo>,
    ty: KExpr<M>,
    body: KExpr<M>,
    mdata: M::MField<Vec<MData>>,
  ) -> Self {
    let addr = fresh_uid();
    Self::all_mdata_with_addr(name, bi, ty, body, mdata, addr)
  }

  pub fn let_(
    name: M::MField<Name>,
    ty: KExpr<M>,