| 422 | ConstantInfo::AxiomInfo(AxiomVal { |
| 423 | cnst: ConstantVal { |
| 424 | name: n("A"), |
| 425 | level_params: vec![], |
| 426 | typ: Expr::cnst(n("B"), vec![]), |
| 427 | }, |
| 428 | is_unsafe: false, |
| 429 | }), |
| 430 | ); |
| 431 | let errors = check(&env); |
| 432 | // B is directly ungrounded |
| 433 | assert!(errors.contains_key(&n("B"))); |
| 434 | // A is transitively ungrounded via Ref(B) |
| 435 | assert!(errors.contains_key(&n("A"))); |
| 436 | assert!(matches!(errors[&n("A")], GroundError::Ref(_))); |
| 437 | } |
| 438 | |
| 439 | #[test] |
| 440 | fn inductive_missing_ctor() { |
| 441 | // Inductive T lists T.mk as a ctor, but T.mk is not in env |
| 442 | let mut env = Env::default(); |
| 443 | env.insert( |
| 444 | n("T"), |
| 445 | ConstantInfo::InductInfo(InductiveVal { |
| 446 | cnst: mk_cv("T"), |
| 447 | num_params: Nat::from(0u64), |