# Documentation

Lean.Meta.DecLevel

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

canAssignMVars : Bool
Instances For
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.

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.

Equations