| 929 | |
| 930 | let interned = env.intern_expr(result); |
| 931 | cache.insert(key, interned.clone()); |
| 932 | interned |
| 933 | } |
| 934 | |
| 935 | /// Inverse of [`instantiate_rev`]: replace each occurrence of the listed |
| 936 | /// fvars in `body` with the appropriate `Var(level)` and shift other |
| 937 | /// loose bvars upward by `n` so the result is closed under `n` new |
| 938 | /// binders. `fvars[0]` becomes `Var(n - 1 + depth)` (outermost), `fvars[n-1]` |
| 939 | /// becomes `Var(depth)` (innermost). |
| 940 | /// |
| 941 | /// Used by `LocalContext::mk_lambda` / `mk_pi` to close a body back into |
| 942 | /// a chain of de Bruijn binders after binder opening. |
| 943 | /// |
| 944 | /// Fast path: returns `body` unchanged when `!body.has_fvars()`. |
| 945 | pub fn abstract_fvars<M: KernelMode>( |