Strict structural alpha-equivalence on already-normalized levels. Direct callers should go through [`level_alpha_eq`] so both sides are normalized first; this helper exists only to avoid re-normalizing at every recursion step.
(a: &Level, b: &Level)
| 64 | /// are normalized first; this helper exists only to avoid re-normalizing |
| 65 | /// at every recursion step. |
| 66 | fn level_alpha_eq_struct(a: &Level, b: &Level) -> Result<(), String> { |
| 67 | match (a.as_data(), b.as_data()) { |
| 68 | (LevelData::Zero(_), LevelData::Zero(_)) => Ok(()), |
| 69 | (LevelData::Succ(a1, _), LevelData::Succ(b1, _)) => { |
| 70 | level_alpha_eq_struct(a1, b1) |
| 71 | }, |
| 72 | (LevelData::Max(a1, a2, _), LevelData::Max(b1, b2, _)) |
| 73 | | (LevelData::Imax(a1, a2, _), LevelData::Imax(b1, b2, _)) => { |
| 74 | level_alpha_eq_struct(a1, b1)?; |
| 75 | level_alpha_eq_struct(a2, b2) |
| 76 | }, |
| 77 | (LevelData::Param(_, _), LevelData::Param(_, _)) => { |
| 78 | // Positional: both sides have the same level_params order, |
| 79 | // so param names should match. But for robustness, just accept. |
| 80 | Ok(()) |
| 81 | }, |
| 82 | (LevelData::Mvar(_, _), _) | (_, LevelData::Mvar(_, _)) => { |
| 83 | Err("unexpected level MVar".into()) |
| 84 | }, |
| 85 | _ => Err(format!( |
| 86 | "level mismatch: {} vs {} ({} vs {})", |
| 87 | level_tag(a), |
| 88 | level_tag(b), |
| 89 | a.pretty(), |
| 90 | b.pretty(), |
| 91 | )), |
| 92 | } |
| 93 | } |
| 94 | |
| 95 | /// Check that two Lean expressions are alpha-equivalent (ignoring binder |
| 96 | /// names, BinderInfo, and Mdata wrappers). |
no test coverage detected