()
| 330 | let mut env = Env::default(); |
| 331 | env.insert( |
| 332 | n("A"), |
| 333 | ConstantInfo::AxiomInfo(AxiomVal { |
| 334 | cnst: ConstantVal { |
| 335 | name: n("A"), |
| 336 | level_params: vec![], |
| 337 | typ: Expr::bvar(Nat::from(0u64)), |
| 338 | }, |
| 339 | is_unsafe: false, |
| 340 | }), |
| 341 | ); |
| 342 | let errors = check(&env); |
| 343 | assert!(errors.contains_key(&n("A"))); |
| 344 | assert!(matches!(errors[&n("A")], GroundError::Var(_, 0))); |
| 345 | } |
| 346 | |
| 347 | #[test] |
| 348 | fn ungrounded_mvar() { |
| 349 | // Axiom A : ?m |
| 350 | let mut env = Env::default(); |
| 351 | env.insert( |
| 352 | n("A"), |