| 290 | sort0(), |
| 291 | Expr::bvar(Nat::from(0u64)), |
| 292 | BinderInfo::Default, |
| 293 | ); |
| 294 | env.insert( |
| 295 | n("f"), |
| 296 | ConstantInfo::DefnInfo(DefinitionVal { |
| 297 | cnst: ConstantVal { name: n("f"), level_params: vec![], typ: sort0() }, |
| 298 | value: body, |
| 299 | hints: ReducibilityHints::Opaque, |
| 300 | safety: DefinitionSafety::Safe, |
| 301 | all: vec![n("f")], |
| 302 | }), |
| 303 | ); |
| 304 | assert!(check(&env).is_empty()); |
| 305 | } |
| 306 | |
| 307 | #[test] |
| 308 | fn ungrounded_missing_ref() { |
| 309 | // Axiom A : B, but B is not in env |
| 310 | let mut env = Env::default(); |
| 311 | env.insert( |
| 312 | n("A"), |