| 664 | /// |
| 665 | /// This matches what Lean4Lean's paper-level theory expects but its |
| 666 | /// implementation doesn't cover (cf. the `sorry` on |
| 667 | /// `NormLevel.subsumption_eval` in `Verify/Level.lean:545`, and the absence |
| 668 | /// of any `geq'_wf`). |
| 669 | fn norm_level_le(l1: &NormLevel, l2: &NormLevel) -> bool { |
| 670 | for (p1, n1) in l1 { |
| 671 | if n1.constant == 0 && n1.var.is_empty() { |
| 672 | continue; |
| 673 | } |
| 674 | if n1.constant != 0 && !covers_const(l2, p1, n1.constant) { |
| 675 | return false; |
| 676 | } |
| 677 | for v in &n1.var { |
| 678 | if !covers_var(l2, p1, v.idx, v.offset) { |
| 679 | return false; |
| 680 | } |
| 681 | } |
| 682 | } |
| 683 | true |
| 684 | } |
| 685 | |
| 686 | /// Entry-wise equality of two normal forms, IGNORING empty entries |
| 687 | /// (constant 0, no vars — pure subsumption bookkeeping). Subsumption |