| 593 | /// which has type Sort 1 (a function type), not Sort 0. |
| 594 | #[test] |
| 595 | fn bad_non_prop_thm() { |
| 596 | let mut env = KEnv::<Meta>::new(); |
| 597 | // type = Sort 0 = Prop |
| 598 | // value = Prop → bvar0 = ∀ (_ : Prop), bvar0 |
| 599 | // But inside the pi body bvar0 refers to the pi's variable (of type Prop). |
| 600 | // infer(value) = Sort(imax 1 0) = Sort 0 = Prop... wait. |
| 601 | // Actually: domain Prop : Sort 1, so l_a = 1. |
| 602 | // Codomain: bvar0 has type Prop. infer(bvar0) = Prop = Sort 0, l_b = 0. |
| 603 | // Pi type: Sort(imax 1 0) = Sort 0 = Prop. |
| 604 | // So the value HAS type Prop, same as the declared type. This should be accepted. |
| 605 | // |
| 606 | // Hmm, looking at the tutorial more carefully: the value is |
| 607 | // arrow (.sort 0) (.bvar 0) |
| 608 | // where .bvar 0 in the ARROW BODY refers to the arrow's own bound var. |
| 609 | // So this is ∀ (_ : Prop), _ where _ is the bound var itself. |
| 610 | // The bound var has type Prop. infer(bvar0) = Prop = Sort 0. |
| 611 | // For this to be valid as a pi body, we need the body's type to be a Sort. |
| 612 | // Sort 0 IS a Sort. So the pi is well-typed: Sort(imax 1 0) = Sort 0 = Prop. |
| 613 | // |
| 614 | // But the tutorial says this is BAD because "The type of a theorem has to be a proposition." |
| 615 | // The theorem's type IS Sort 0 = Prop. And the value also has type Prop. |
| 616 | // Maybe the BAD part is that a theorem's declared type must be a proposition |
| 617 | // (i.e., have type Prop), but Sort 0 itself has type Sort 1, not Prop. |
| 618 | // |
| 619 | // Actually: the declared type of the theorem is `.sort 0`. The TYPE OF `.sort 0` is |
| 620 | // `.sort 1`. For a theorem, we check `infer(ty)` and `ensure_sort` — that gives level 1. |
| 621 | // Then we should additionally check that this level IS 0 (Prop). |
| 622 | // The kernel currently doesn't enforce "theorem types must be Prop." |
| 623 | // |
| 624 | // This is a theorem-specific check that the zero kernel may not implement. |
| 625 | let ty = sort0(); // Sort 0 = Prop |
| 626 | let val = pi(sort0(), var(0)); // Prop → bvar0 |
| 627 | let (id, c) = mk_thm("nonPropThm", 0, vec![], ty, val); |
| 628 | env.insert(id.clone(), c); |
| 629 | // The lean kernel requires theorems' types to be Prop (level 0). |
| 630 | // Sort 0 has type Sort 1, so the theorem type is in Sort 1, not Prop. |
| 631 | check_rejects(&mut env, &id); |
| 632 | } |
| 633 | } |