| 330 | |
| 331 | #[test] |
| 332 | fn test_basic_unification() { |
| 333 | let mut arena = Arena::new(); |
| 334 | let env = Environment::new(); |
| 335 | let ctx = Context::new(); |
| 336 | let mut unifier = Unifier::new(); |
| 337 | |
| 338 | let var0 = arena.mk_var(0); |
| 339 | let var1 = arena.mk_var(1); |
| 340 | |
| 341 | // ?0 = var0 |
| 342 | let mvar0 = arena.mk_mvar(MetaVarId::new(0)); |
| 343 | unifier.unify(mvar0, var0); |
| 344 | |
| 345 | unifier.solve(&mut arena, &env, &ctx).unwrap(); |
| 346 | |
| 347 | assert!(unifier.is_solved()); |
| 348 | assert!(unifier.substitution().is_assigned(MetaVarId::new(0))); |
| 349 | } |
| 350 | |
| 351 | #[test] |
| 352 | fn test_occurs_check() { |