| 1319 | let _ = fv0; // silence unused |
| 1320 | } |
| 1321 | |
| 1322 | #[test] |
| 1323 | fn abstract_fvars_lifts_loose_bvars() { |
| 1324 | let mut env = InternTable::<Anon>::new(); |
| 1325 | let fv0 = AE::fvar(FVarId(0), ()); |
| 1326 | let v0 = AE::var(0, ()); |
| 1327 | let app = AE::app(fv0, v0); |
| 1328 | // Wrap one new binder around `app`; fv0 → Var(0); existing Var(0) |
| 1329 | // (loose) shifts up to Var(1). |
| 1330 | let result = abstract_fvars(&mut env, &app, &[FVarId(0)]); |
| 1331 | let expected = AE::app(AE::var(0, ()), AE::var(1, ())); |
| 1332 | assert_eq!(result, expected); |
| 1333 | } |
| 1334 | |
| 1335 | #[test] |