| 350 | let mut env = Env::default(); |
| 351 | env.insert( |
| 352 | n("A"), |
| 353 | ConstantInfo::AxiomInfo(AxiomVal { |
| 354 | cnst: ConstantVal { |
| 355 | name: n("A"), |
| 356 | level_params: vec![], |
| 357 | typ: Expr::mvar(n("m")), |
| 358 | }, |
| 359 | is_unsafe: false, |
| 360 | }), |
| 361 | ); |
| 362 | let errors = check(&env); |
| 363 | assert!(errors.contains_key(&n("A"))); |
| 364 | assert!(matches!(errors[&n("A")], GroundError::MVar(_))); |
| 365 | } |
| 366 | |
| 367 | #[test] |
| 368 | fn ungrounded_level_param() { |
| 369 | // Axiom A : Sort (Param "u"), but "u" not in level_params |
| 370 | let mut env = Env::default(); |
| 371 | env.insert( |
| 372 | n("A"), |