• canAssignMVars : Bool

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

Instances For

    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.

    Instances For