| 370 | let mut env = Env::default(); |
| 371 | env.insert( |
| 372 | n("A"), |
| 373 | ConstantInfo::AxiomInfo(AxiomVal { |
| 374 | cnst: ConstantVal { |
| 375 | name: n("A"), |
| 376 | level_params: vec![], // u is not declared |
| 377 | typ: Expr::sort(Level::param(n("u"))), |
| 378 | }, |
| 379 | is_unsafe: false, |
| 380 | }), |
| 381 | ); |
| 382 | let errors = check(&env); |
| 383 | assert!(errors.contains_key(&n("A"))); |
| 384 | assert!(matches!(errors[&n("A")], GroundError::Level(_, _))); |
| 385 | } |
| 386 | |
| 387 | #[test] |
| 388 | fn grounded_level_param_when_declared() { |
| 389 | // Axiom A.{u} : Sort u — "u" is declared |
| 390 | let mut env = Env::default(); |