Like [`Self::open_binder`] but also returns the fvar `KExpr` itself (for callers that need to record it in a Vec for later abstract_fvars / structural identity comparisons).
(
&mut self,
name: M::MField<ix_common::env::Name>,
bi: M::MField<ix_common::env::BinderInfo>,
ty: KExpr<M>,
body: &KExpr<M>,
)
| 566 | &mut self, |
| 567 | ty: KExpr<M>, |
| 568 | body: &KExpr<M>, |
| 569 | ) -> (KExpr<M>, FVarId) { |
| 570 | let name = M::meta_field(ix_common::env::Name::anon()); |
| 571 | let bi = M::meta_field(ix_common::env::BinderInfo::Default); |
| 572 | self.open_binder(name, bi, ty, body) |
| 573 | } |
| 574 | |
| 575 | /// Like [`Self::open_binder`] but also returns the fvar `KExpr` itself |
| 576 | /// (for callers that need to record it in a Vec for later |
| 577 | /// abstract_fvars / structural identity comparisons). |
| 578 | pub fn open_binder_with_fv( |
| 579 | &mut self, |
| 580 | name: M::MField<ix_common::env::Name>, |
| 581 | bi: M::MField<ix_common::env::BinderInfo>, |
| 582 | ty: KExpr<M>, |
| 583 | body: &KExpr<M>, |
| 584 | ) -> (KExpr<M>, KExpr<M>, FVarId) { |
no test coverage detected