| 283 | |
| 284 | #[test] |
| 285 | fn lctx_push_find_truncate() { |
| 286 | let mut ngen = NameGenerator::new(); |
| 287 | let mut lctx: LocalContext<Anon> = LocalContext::new(); |
| 288 | |
| 289 | let id1 = ngen.fresh(); |
| 290 | let id2 = ngen.fresh(); |
| 291 | let ty1 = AE::sort(AU::zero()); |
| 292 | let ty2 = AE::sort(AU::succ(AU::zero())); |
| 293 | |
| 294 | lctx.push( |
| 295 | id1, |
| 296 | LocalDecl::CDecl { name: ANON_NAME, bi: ANON_BI, ty: ty1.clone() }, |
| 297 | ); |
| 298 | lctx.push( |
| 299 | id2, |
| 300 | LocalDecl::CDecl { name: ANON_NAME, bi: ANON_BI, ty: ty2.clone() }, |
| 301 | ); |
| 302 | |
| 303 | assert_eq!(lctx.len(), 2); |
| 304 | assert_eq!(lctx.find(id1).map(|d| d.ty()), Some(&ty1)); |
| 305 | assert_eq!(lctx.find(id2).map(|d| d.ty()), Some(&ty2)); |
| 306 | |
| 307 | lctx.truncate(1); |
| 308 | assert_eq!(lctx.len(), 1); |
| 309 | assert!(lctx.find(id2).is_none()); |
| 310 | assert_eq!(lctx.find(id1).map(|d| d.ty()), Some(&ty1)); |
| 311 | |
| 312 | lctx.truncate(0); |
| 313 | assert!(lctx.is_empty()); |
| 314 | assert!(lctx.find(id1).is_none()); |
| 315 | } |
| 316 | |
| 317 | #[test] |
| 318 | fn fvar_distinct_ids_distinct_hashes() { |