def Auto.Level.hasCurrentDepthLevelMVar : Lean.Level → Lean.MetaM Bool

Equations

• Auto.Level.hasCurrentDepthLevelMVar Lean.Level.zero = pure false
• Auto.Level.hasCurrentDepthLevelMVar l.succ = Auto.Level.hasCurrentDepthLevelMVar l
• Auto.Level.hasCurrentDepthLevelMVar (l₁.max l₂) = or <$> Auto.Level.hasCurrentDepthLevelMVar l₁ <*> Auto.Level.hasCurrentDepthLevelMVar l₂
• Auto.Level.hasCurrentDepthLevelMVar (l₁.imax l₂) = or <$> Auto.Level.hasCurrentDepthLevelMVar l₁ <*> Auto.Level.hasCurrentDepthLevelMVar l₂
• Auto.Level.hasCurrentDepthLevelMVar (Lean.Level.param a) = pure false
• Auto.Level.hasCurrentDepthLevelMVar (Lean.Level.mvar id) = not <$> id.isReadOnly

def Auto.Level.collectLevelMVars (l : Lean.Level) : Lean.MetaM (Array Lean.LMVarId)

Equations

• Auto.Level.collectLevelMVars l = do let l ← Lean.instantiateLevelMVars l let hset : Std.HashSet Lean.LMVarId := Auto.Level.collectLevelMVars.go l pure hset.toArray

def Auto.Level.collectLevelMVars.go : Lean.Level → Std.HashSet Lean.LMVarId

Equations

• Auto.Level.collectLevelMVars.go Lean.Level.zero = ∅
• Auto.Level.collectLevelMVars.go l.succ = Auto.Level.collectLevelMVars.go l
• Auto.Level.collectLevelMVars.go (l₁.max l₂) = Auto.mergeHashSet (Auto.Level.collectLevelMVars.go l₁) (Auto.Level.collectLevelMVars.go l₂)
• Auto.Level.collectLevelMVars.go (l₁.imax l₂) = Auto.mergeHashSet (Auto.Level.collectLevelMVars.go l₁) (Auto.Level.collectLevelMVars.go l₂)
• Auto.Level.collectLevelMVars.go (Lean.Level.param a) = ∅
• Auto.Level.collectLevelMVars.go (Lean.Level.mvar id) = Std.HashSet.emptyWithCapacity.insert id

def Auto.Level.findParam? (p : Lean.Name → Bool) : Lean.Level → Option Lean.Name

Equations

• Auto.Level.findParam? p Lean.Level.zero = none
• Auto.Level.findParam? p l.succ = Auto.Level.findParam? p l
• Auto.Level.findParam? p (l₁.max l₂) = (Auto.Level.findParam? p l₁).orElse fun (x : Unit) => Auto.Level.findParam? p l₂
• Auto.Level.findParam? p (l₁.imax l₂) = (Auto.Level.findParam? p l₁).orElse fun (x : Unit) => Auto.Level.findParam? p l₂
• Auto.Level.findParam? p (Lean.Level.param a) = match p a with | true => some a | false => none
• Auto.Level.findParam? p (Lean.Level.mvar id) = none