Push an `LDecl` for a let-bound fvar and instantiate the body. Returns the opened body and the fresh fvar id. Mirrors `withLetDecl`-shaped flows (e.g. inductive validation that needs to model the let value for downstream WHNF zeta-reduction).
(
&mut self,
name: M::MField<ix_common::env::Name>,
ty: KExpr<M>,
val: KExpr<M>,
body: &KExpr<M>,
)
| 596 | ty: KExpr<M>, |
| 597 | body: &KExpr<M>, |
| 598 | ) -> (KExpr<M>, KExpr<M>, FVarId) { |
| 599 | let name = M::meta_field(ix_common::env::Name::anon()); |
| 600 | let bi = M::meta_field(ix_common::env::BinderInfo::Default); |
| 601 | self.open_binder_with_fv(name, bi, ty, body) |
| 602 | } |
| 603 | |
| 604 | /// Push an `LDecl` for a let-bound fvar and instantiate the body. Returns |
| 605 | /// the opened body and the fresh fvar id. Mirrors `withLetDecl`-shaped |
| 606 | /// flows (e.g. inductive validation that needs to model the let value |
| 607 | /// for downstream WHNF zeta-reduction). |
| 608 | pub fn open_let( |
| 609 | &mut self, |
| 610 | name: M::MField<ix_common::env::Name>, |
| 611 | ty: KExpr<M>, |
| 612 | val: KExpr<M>, |
| 613 | body: &KExpr<M>, |
nothing calls this directly
no test coverage detected