| 478 | }), |
| 479 | ); |
| 480 | env.insert( |
| 481 | n("T.mk"), |
| 482 | ConstantInfo::AxiomInfo(AxiomVal { |
| 483 | cnst: mk_cv("T.mk"), |
| 484 | is_unsafe: false, |
| 485 | }), |
| 486 | ); |
| 487 | let errors = check(&env); |
| 488 | assert!(errors.contains_key(&n("T"))); |
| 489 | assert!(matches!( |
| 490 | &errors[&n("T")], |
| 491 | GroundError::Indc(b) if b.1.is_some() |
| 492 | )); |
| 493 | } |
| 494 | |
| 495 | #[test] |
| 496 | fn binding_increments_depth() { |
| 497 | // fun (_ : Sort 0) => #0 is grounded (bvar under 1 binder) |
| 498 | // but fun (_ : Sort 0) => #1 is ungrounded (bvar escapes) |
| 499 | let mut env = Env::default(); |
| 500 | |
| 501 | // Grounded case |
| 502 | env.insert( |
| 503 | n("ok"), |
| 504 | ConstantInfo::DefnInfo(DefinitionVal { |
| 505 | cnst: ConstantVal { name: n("ok"), level_params: vec![], typ: sort0() }, |
| 506 | value: Expr::lam( |
| 507 | Name::anon(), |
| 508 | sort0(), |
| 509 | Expr::bvar(Nat::from(0u64)), |
| 510 | BinderInfo::Default, |
| 511 | ), |
| 512 | hints: ReducibilityHints::Opaque, |
| 513 | safety: DefinitionSafety::Safe, |
| 514 | all: vec![n("ok")], |
| 515 | }), |
| 516 | ); |
| 517 | |
| 518 | // Ungrounded case |
| 519 | env.insert( |
| 520 | n("bad"), |
| 521 | ConstantInfo::DefnInfo(DefinitionVal { |
| 522 | cnst: ConstantVal { |
| 523 | name: n("bad"), |
| 524 | level_params: vec![], |
| 525 | typ: sort0(), |
| 526 | }, |
| 527 | value: Expr::lam( |
| 528 | Name::anon(), |
| 529 | sort0(), |
| 530 | Expr::bvar(Nat::from(1u64)), // escapes the single binder |