Open a binder by minting a fresh [`FVarId`], pushing a `CDecl` to `lctx`, and instantiating `body` so its `Var(0)` becomes the new fvar (with `Var(>=1)` shifting down). Returns the opened body and the fresh fvar id (the caller may pass `_` to discard). Mirrors lean4lean's `withLocalDecl` in shape; differs in that the caller is responsible for `lctx.truncate(saved_len)` when leaving the binder sco
(
&mut self,
name: M::MField<ix_common::env::Name>,
bi: M::MField<ix_common::env::BinderInfo>,
ty: KExpr<M>,
body: &KExpr<M>,
)
| 535 | // ----------------------------------------------------------------------- |
| 536 | // Free-variable binder opening helpers |
| 537 | // ----------------------------------------------------------------------- |
| 538 | |
| 539 | /// Open a binder by minting a fresh [`FVarId`], pushing a `CDecl` to |
| 540 | /// `lctx`, and instantiating `body` so its `Var(0)` becomes the new |
| 541 | /// fvar (with `Var(>=1)` shifting down). Returns the opened body and |
| 542 | /// the fresh fvar id (the caller may pass `_` to discard). |
| 543 | /// |
| 544 | /// Mirrors lean4lean's `withLocalDecl` in shape; differs in that the |
| 545 | /// caller is responsible for `lctx.truncate(saved_len)` when leaving |
| 546 | /// the binder scope. |
| 547 | pub fn open_binder( |
| 548 | &mut self, |
| 549 | name: M::MField<ix_common::env::Name>, |
| 550 | bi: M::MField<ix_common::env::BinderInfo>, |
| 551 | ty: KExpr<M>, |
| 552 | body: &KExpr<M>, |
no test coverage detected