From ef8fecff796783bcaff0cdc887a7f61ca979dd33 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 3 Apr 2022 08:18:14 -0700 Subject: [PATCH] feat: add `Level.geq` --- src/Lean/Level.lean | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/src/Lean/Level.lean b/src/Lean/Level.lean index 05d1b41ce8..744ca98773 100644 --- a/src/Lean/Level.lean +++ b/src/Lean/Level.lean @@ -553,6 +553,24 @@ def mkNaryMax : List Level → Level | none => u | u => u +def geq (u v : Level) : Bool := + go u.normalize v.normalize +where + go (u v : Level) : Bool := + u == v || + match u, v with + | u, zero _ => true + | u, max v₁ v₂ _ => go u v₁ && go u v₂ + | max u₁ u₂ _, v => go u₁ v || go u₂ v + | u, imax v₁ v₂ _ => go u v₁ && go u v₂ + | imax u₁ u₂ _, v => go u₂ v + | succ u _, succ v _ => go u v + | _, _ => + let v' := v.getLevelOffset + (u.getLevelOffset == v' || v'.isZero) + && u.getOffset ≥ v.getOffset +termination_by _ u v => (u, v) + end Level open Std (HashMap HashSet PHashMap PHashSet)