structure Lean.Meta.DecLevelContext : Type

• canAssignMVars : Bool

  If true, then decAux? ?m returns a fresh metavariable ?n s.t. ?m := ?n+1.

def Lean.Meta.decLevel? (u : Lean.Level) : Lean.MetaM (Option Lean.Level)

def Lean.Meta.decLevel (u : Lean.Level) : Lean.MetaM Lean.Level

def Lean.Meta.getDecLevel (type : Lean.Expr) : Lean.MetaM Lean.Level

This method is useful for inferring universe level parameters for function that take arguments such as {α : Type u}. Recall that Type u is Sort (u+1) in Lean. Thus, given α, we must infer its universe level, and then decrement 1 to obtain u.