| 445 | ConstantInfo::InductInfo(InductiveVal { |
| 446 | cnst: mk_cv("T"), |
| 447 | num_params: Nat::from(0u64), |
| 448 | num_indices: Nat::from(0u64), |
| 449 | all: vec![n("T")], |
| 450 | ctors: vec![n("T.mk")], |
| 451 | num_nested: Nat::from(0u64), |
| 452 | is_rec: false, |
| 453 | is_unsafe: false, |
| 454 | is_reflexive: false, |
| 455 | }), |
| 456 | ); |
| 457 | let errors = check(&env); |
| 458 | assert!(errors.contains_key(&n("T"))); |
| 459 | assert!(matches!(errors[&n("T")], GroundError::Indc(_))); |
| 460 | } |
| 461 | |
| 462 | #[test] |
| 463 | fn inductive_ctor_wrong_kind() { |
| 464 | // Inductive T lists T.mk as a ctor, but T.mk is an axiom not a ctor |
| 465 | let mut env = Env::default(); |
| 466 | env.insert( |
| 467 | n("T"), |
| 468 | ConstantInfo::InductInfo(InductiveVal { |
| 469 | cnst: mk_cv("T"), |
| 470 | num_params: Nat::from(0u64), |
| 471 | num_indices: Nat::from(0u64), |
| 472 | all: vec![n("T")], |
| 473 | ctors: vec![n("T.mk")], |
| 474 | num_nested: Nat::from(0u64), |
| 475 | is_rec: false, |
| 476 | is_unsafe: false, |
| 477 | is_reflexive: false, |
| 478 | }), |
| 479 | ); |
| 480 | env.insert( |