From a9f3aa086d5c918a0b598eef237e63bf50c34a8a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 30 Oct 2019 18:23:12 -0700
Subject: [PATCH] feat: add `Level.dec`

---
 library/Init/Lean/Level.lean | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/library/Init/Lean/Level.lean b/library/Init/Lean/Level.lean
index f1c042294f..f63fb1be22 100644
--- a/library/Init/Lean/Level.lean
+++ b/library/Init/Lean/Level.lean
@@ -62,6 +62,10 @@ def isMVar : Level → Bool
 | mvar _ => true
 | _      => false
 
+def mvarId! : Level → Name
+| mvar mvarId => mvarId
+| _           => panic! "metavariable expected"
+
 /-- If result is true, then forall assignments `A` which assigns all parameters and metavariables occuring
     in `l`, `l[A] != zero` -/
 def isNeverZero : Level → Bool
@@ -264,6 +268,17 @@ partial def normalize : Level → Level
 def isEquiv (u v : Level) : Bool :=
 u == v || u.normalize == v.normalize
 
+/-- Reduce (if possible) universe level by 1 -/
+def dec : Level → Option Level
+| zero       => none
+| param _    => none
+| mvar _     => none
+| succ l     => l
+| max l₁ l₂  => max <$> dec l₁ <*> dec l₂
+/- Remark: `max` in the following line is not a typo.
+   If `dec l₂` succeeds, then `imax l₁ l₂` is equivalent to `max l₁ l₂`. -/
+| imax l₁ l₂ => max <$> dec l₁ <*> dec l₂
+
 /- Level to Format -/
 namespace LevelToFormat
 inductive Result