| 424 | Self::lam_mdata(name, bi, ty, body, no_mdata::<M>()) |
| 425 | } |
| 426 | |
| 427 | /// Compute the content hash for [`KExpr::lam_mdata`]. |
| 428 | /// |
| 429 | fn lam_mdata_with_addr( |
| 430 | name: M::MField<Name>, |
| 431 | bi: M::MField<BinderInfo>, |
| 432 | ty: KExpr<M>, |
| 433 | body: KExpr<M>, |
| 434 | mdata: M::MField<Vec<MData>>, |
| 435 | addr: Addr, |
| 436 | ) -> Self { |
| 437 | let info = mk_info::<M>( |
| 438 | addr, |
| 439 | ty.lbr().max(body.lbr().saturating_sub(1)), |
| 440 | ty.count_0(), |
| 441 | ty.has_fvars() || body.has_fvars(), |
| 442 | mdata, |
| 443 | ); |
| 444 | KExpr::new(ExprData::Lam(name, bi, ty, body, info)) |
| 445 | } |