Documentation

Lean.Meta.DecLevel

source
structure Lean.Meta.DecLevelContext:
Type

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

    canAssignMVars : Bool
source
def Lean.Meta.decLevel? (u : Lean.Level) :
Lean.MetaM (Option Lean.Level)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.decLevel (u : Lean.Level) :
Lean.MetaM Lean.Level
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.getDecLevel (type : Lean.Expr) :
Lean.MetaM Lean.Level
Equations