| 445 | /// tut06_bad01: definition with duplicate level params [u, u] |
| 446 | #[test] |
| 447 | fn bad_duplicate_level_params() { |
| 448 | let mut env = KEnv::<Meta>::new(); |
| 449 | let (id, c) = mk_defn( |
| 450 | "tut06_bad01", |
| 451 | 2, // claims 2 level params |
| 452 | vec![mk_name("u"), mk_name("u")], // duplicate! |
| 453 | sort(usucc(uzero())), // Sort 1 |
| 454 | sort0(), // Sort 0 |
| 455 | ReducibilityHints::Opaque, |
| 456 | ); |
| 457 | env.insert(id.clone(), c); |
| 458 | check_rejects(&mut env, &id); |
| 459 | } |
| 460 | |
| 461 | // ========================================================================== |
| 462 | // Batch 7: forallSortBad and nonPropThm (Tutorial.lean lines 41–61) |