source
structure Lean.Meta.DecLevelContext :
Type

- canAssignMVars : Bool

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

Instances For

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

- One or more equations did not get rendered due to their size.

Instances For

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

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Meta.getDecLevel (type : Expr) :
MetaM 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`.

Equations

- Lean.Meta.getDecLevel type = do let __do_lift ← Lean.Meta.getLevel type Lean.Meta.decLevel __do_lift

Instances For

source
def Lean.Meta.getDecLevel? (type : Expr) :
MetaM (Option Level)
Equations

- Lean.Meta.getDecLevel? type = do let __do_lift ← Lean.Meta.getLevel type Lean.Meta.decLevel? __do_lift

Instances For