()
| 723 | |
| 724 | #[test] |
| 725 | fn infer_all() { |
| 726 | let mut env = test_env(); |
| 727 | let mut tc = TypeChecker::new(&mut env); |
| 728 | // ∀ (x : Sort 0). Sort 0 : Sort 1 |
| 729 | let all = AE::all((), (), sort0(), sort0()); |
| 730 | let ty = tc.infer(&all).unwrap(); |
| 731 | assert!(matches!(ty.data(), ExprData::Sort(..))); |
| 732 | } |
| 733 | |
| 734 | #[test] |
| 735 | fn infer_nat_lit() { |