()
| 670 | |
| 671 | #[test] |
| 672 | fn infer_sort() { |
| 673 | let mut env = test_env(); |
| 674 | let mut tc = TypeChecker::new(&mut env); |
| 675 | // Sort 0 : Sort 1 |
| 676 | let ty = tc.infer(&sort0()).unwrap(); |
| 677 | assert!(matches!(ty.data(), ExprData::Sort(u, _) if !u.is_zero())); |
| 678 | } |
| 679 | |
| 680 | #[test] |
| 681 | fn infer_var() { |