| 1156 | } |
| 1157 | |
| 1158 | #[test] |
| 1159 | fn subst_bound_var_unchanged() { |
| 1160 | let mut env = InternTable::<Anon>::new(); |
| 1161 | let nat = AE::cnst(KId::new(mk_addr("Nat"), ()), Box::new([])); |
| 1162 | let v0 = AE::var(0, ()); |
| 1163 | // λ(_:Nat). Var(0) — body is lambda-bound, closed under binder |
| 1164 | let lam = AE::lam((), (), nat, v0); |
| 1165 | let arg = AE::nat(Nat::from(3u64), mk_addr("3")); |
| 1166 | let result = subst(&mut env, &lam, &arg, 0); |
| 1167 | assert!(result.ptr_eq(&lam)); |
| 1168 | } |
| 1169 | |
| 1170 | #[test] |
| 1171 | fn lift_var() { |
| 1172 | let mut env = InternTable::<Anon>::new(); |
| 1173 | let v0 = AE::var(0, ()); |
| 1174 | // lift(Var(0), shift=1, cutoff=0) → Var(1) |
| 1175 | let result = lift(&mut env, &v0, 1, 0); |
| 1176 | assert_eq!(result, AE::var(1, ())); |