Method app_mdata_with_addr

crates/kernel/src/expr.rs:371–385

(
    f: KExpr<M>,
    a: KExpr<M>,
    mdata: M::MField<Vec<MData>>,
    addr: Addr,
  )

    univs: Box<[KUniv<M>]>,
    mdata: M::MField<Vec<MData>>,
    addr: Addr,
  ) -> Self {
    KExpr::new(ExprData::Const(
      id,
      univs,
      mk_info::<M>(addr, 0, 0, false, mdata),
    ))
  }

  pub fn cnst_mdata(
    id: KId<M>,
    univs: Box<[KUniv<M>]>,
    mdata: M::MField<Vec<MData>>,
  ) -> Self {
    let addr = fresh_uid();
    Self::cnst_mdata_with_addr(id, univs, mdata, addr)
  }