| 512 | /// "post-normalize subterms are normalized" silently invalid). |
| 513 | #[test] |
| 514 | fn level_normalize_idempotent() { |
| 515 | let u = p("u"); |
| 516 | let v = p("v"); |
| 517 | let cases = [ |
| 518 | m(s(z()), s(z())), |
| 519 | m(z(), u.clone()), |
| 520 | m(u.clone(), m(u.clone(), v.clone())), |
| 521 | im(u.clone(), s(v.clone())), |
| 522 | im(u, z()), |
| 523 | m(s(v.clone()), s(s(v))), |
| 524 | ]; |
| 525 | for l in &cases { |
| 526 | let n1 = normalize_level(l); |
| 527 | let n2 = normalize_level(&n1); |
| 528 | assert_eq!(n1, n2, "normalize_level not idempotent on {}", l.pretty()); |
| 529 | } |
| 530 | } |
| 531 | } |