Method let_mdata_with_addr

crates/kernel/src/expr.rs:539–556

(
    name: M::MField<Name>,
    ty: KExpr<M>,
    val: KExpr<M>,
    body: KExpr<M>,
    non_dep: bool,
    mdata: M::MField<Vec<MData>>,
    addr: Addr,
  )

  pub fn prj(id: KId<M>, field: u64, val: KExpr<M>) -> Self {
    Self::prj_mdata(id, field, val, no_mdata::<M>())
  }

  fn prj_mdata_with_addr(
    id: KId<M>,
    field: u64,
    val: KExpr<M>,
    mdata: M::MField<Vec<MData>>,
    addr: Addr,
  ) -> Self {
    let info =
      mk_info::<M>(addr, val.lbr(), val.count_0(), val.has_fvars(), mdata);
    KExpr::new(ExprData::Prj(id, field, val, info))
  }

  pub fn prj_mdata(
    id: KId<M>,
    field: u64,
    val: KExpr<M>,
    mdata: M::MField<Vec<MData>>,
  ) -> Self {
    let addr = fresh_uid();