()
| 700 | |
| 701 | #[test] |
| 702 | fn infer_lam() { |
| 703 | let mut env = test_env(); |
| 704 | let mut tc = TypeChecker::new(&mut env); |
| 705 | // λ (x : Sort 0). x : ∀ (x : Sort 0). Sort 0 |
| 706 | let lam = AE::lam((), (), sort0(), AE::var(0, ())); |
| 707 | let ty = tc.infer(&lam).unwrap(); |
| 708 | assert!(matches!(ty.data(), ExprData::All(..))); |
| 709 | } |
| 710 | |
| 711 | #[test] |
| 712 | fn infer_app() { |