| 425 | /// The type has a let that reduces to Sort 0 = Prop. aProp : Prop. |
| 426 | #[test] |
| 427 | fn good_let_red() { |
| 428 | let mut env = KEnv::<Meta>::new(); |
| 429 | let (ap_id, ap_c) = mk_axiom("aProp", 0, vec![], sort0()); |
| 430 | env.insert(ap_id, ap_c); |
| 431 | |
| 432 | // type: let x : Sort 1 := Sort 0; x — reduces to Sort 0 = Prop |
| 433 | let ty = let_(sort1(), sort0(), var(0)); |
| 434 | let val = cnst("aProp", &[]); |
| 435 | let (id, c) = |
| 436 | mk_defn("letRed", 0, vec![], ty, val, ReducibilityHints::Opaque); |
| 437 | env.insert(id.clone(), c); |
| 438 | check_accepts(&mut env, &id); |
| 439 | } |
| 440 | |
| 441 | // ========================================================================== |
| 442 | // Batch 6: Duplicate level params (Tutorial.lean line 98–106) |