Method prj_mdata

crates/kernel/src/expr.rs:601–609

(
    id: KId<M>,
    field: u64,
    val: KExpr<M>,
    mdata: M::MField<Vec<MData>>,
  )

    Self::lam_mdata_with_addr(name, bi, ty, body, mdata, addr)
  }

  pub fn all(
    name: M::MField<Name>,
    bi: M::MField<BinderInfo>,
    ty: KExpr<M>,
    body: KExpr<M>,
  ) -> Self {
    Self::all_mdata(name, bi, ty, body, no_mdata::<M>())
  }

  fn all_mdata_with_addr(
    name: M::MField<Name>,