Documentation

Lean.Meta.DecLevel

structure Lean.Meta.DecLevelContext :

Type

canAssignMVars : Bool

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

Lean.MetaM (Option Lean.Level)

Equations

Lean.Meta.decLevel? u = do let mctx ← Lean.getMCtx let a ← ReaderT.run (Lean.Meta.decAux? u) { canAssignMVars := true } match a with | some v => pure (some v) | none => do modify fun s => { mctx := mctx, cache := s.cache, zetaFVarIds := s.zetaFVarIds, postponed := s.postponed } pure none

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

Lean.MetaM Lean.Level

Equations

Lean.Meta.decLevel u = do let a ← Lean.Meta.decLevel? u match a with | some u => pure u | none => Lean.throwError (Lean.toMessageData "invalid universe level, " ++ Lean.toMessageData u ++ Lean.toMessageData " is not greater than 0")

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

Lean.MetaM Lean.Level

Equations

Lean.Meta.getDecLevel type = do let a ← Lean.Meta.getLevel type Lean.Meta.decLevel a