def Lean.setEnv {m : Type → Type} [Lean.MonadEnv m] (env : Lean.Environment) : m Unit

Equations

• Lean.setEnv env = Lean.modifyEnv fun x => env

def Lean.withEnv {m : Type → Type} {α : Type} [Monad m] [MonadFinally m] [Lean.MonadEnv m] (env : Lean.Environment) (x : m α) : m α

Equations

• Lean.withEnv env x = do let saved ← Lean.getEnv tryFinally (do Lean.setEnv env x) (Lean.setEnv saved)

def Lean.isInductive {m : Type → Type} [Monad m] [Lean.MonadEnv m] (declName : Lake.Name) : m Bool

Equations

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

def Lean.isRecCore (env : Lean.Environment) (declName : Lake.Name) : Bool

Equations

• Lean.isRecCore env declName = match Lean.Environment.find? env declName with | some (Lean.ConstantInfo.recInfo val) => true | x => false

def Lean.isRec {m : Type → Type} [Monad m] [Lean.MonadEnv m] (declName : Lake.Name) : m Bool

Equations

• Lean.isRec declName = do let __do_lift ← Lean.getEnv pure (Lean.isRecCore __do_lift declName)

@[inline]

def Lean.withoutModifyingEnv {m : Type → Type} [Monad m] [Lean.MonadEnv m] [MonadFinally m] {α : Type} (x : m α) : m α

Equations

• Lean.withoutModifyingEnv x = do let env ← Lean.getEnv tryFinally x (Lean.setEnv env)

@[inline]

def Lean.withoutModifyingEnv' {m : Type → Type} [Monad m] [Lean.MonadEnv m] [MonadFinally m] {α : Type} (x : m α) : m (α × Lean.Environment)

Similar to withoutModifyingEnv, but also returns the updated environment

Equations

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

@[inline]

def Lean.matchConst {m : Type → Type} {α : Type} [Monad m] [Lean.MonadEnv m] (e : Lean.Expr) (failK : Unit → m α) (k : Lean.ConstantInfo → List Lean.Level → m α) : m α

Equations

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

@[inline]

def Lean.matchConstInduct {m : Type → Type} {α : Type} [Monad m] [Lean.MonadEnv m] (e : Lean.Expr) (failK : Unit → m α) (k : Lean.InductiveVal → List Lean.Level → m α) : m α

Equations

• Lean.matchConstInduct e failK k = Lean.matchConst e failK fun cinfo us => match cinfo with | Lean.ConstantInfo.inductInfo val => k val us | x => failK ()

@[inline]

def Lean.matchConstCtor {m : Type → Type} {α : Type} [Monad m] [Lean.MonadEnv m] (e : Lean.Expr) (failK : Unit → m α) (k : Lean.ConstructorVal → List Lean.Level → m α) : m α

Equations

• Lean.matchConstCtor e failK k = Lean.matchConst e failK fun cinfo us => match cinfo with | Lean.ConstantInfo.ctorInfo val => k val us | x => failK ()

@[inline]

def Lean.matchConstRec {m : Type → Type} {α : Type} [Monad m] [Lean.MonadEnv m] (e : Lean.Expr) (failK : Unit → m α) (k : Lean.RecursorVal → List Lean.Level → m α) : m α

Equations

• Lean.matchConstRec e failK k = Lean.matchConst e failK fun cinfo us => match cinfo with | Lean.ConstantInfo.recInfo val => k val us | x => failK ()

def Lean.hasConst {m : Type → Type} [Monad m] [Lean.MonadEnv m] (constName : Lake.Name) : m Bool

Equations

• Lean.hasConst constName = do let __do_lift ← Lean.getEnv pure (Lean.Environment.contains __do_lift constName)

def Lean.mkAuxName {m : Type → Type} [Monad m] [Lean.MonadEnv m] (baseName : Lake.Name) (idx : Nat) : m Lake.Name

Equations

• Lean.mkAuxName baseName idx = do let __do_lift ← Lean.getEnv pure (Lean.mkAuxNameAux __do_lift baseName idx)

def Lean.getConstInfo {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] (constName : Lake.Name) : m Lean.ConstantInfo

Equations

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

def Lean.mkConstWithLevelParams {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] (constName : Lake.Name) : m Lean.Expr

Equations

• Lean.mkConstWithLevelParams constName = do let info ← Lean.getConstInfo constName pure (Lean.mkConst constName (List.map Lean.mkLevelParam (Lean.ConstantInfo.levelParams info)))

def Lean.getConstInfoDefn {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] (constName : Lake.Name) : m Lean.DefinitionVal

Equations

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

def Lean.getConstInfoInduct {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] (constName : Lake.Name) : m Lean.InductiveVal

Equations

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

def Lean.getConstInfoCtor {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] (constName : Lake.Name) : m Lean.ConstructorVal

Equations

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

def Lean.getConstInfoRec {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] (constName : Lake.Name) : m Lean.RecursorVal

Equations

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

@[inline]

def Lean.matchConstStruct {m : Type → Type} {α : Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] (e : Lean.Expr) (failK : Unit → m α) (k : Lean.InductiveVal → List Lean.Level → Lean.ConstructorVal → m α) : m α

Equations

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

unsafe def Lean.evalConst {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] [Lean.MonadOptions m] (α : Type) (constName : Lake.Name) : m α

Equations

• Lean.evalConst α constName = do let __do_lift ← Lean.getEnv let __do_lift_1 ← Lean.getOptions Lean.ofExcept (Lean.Environment.evalConst α __do_lift __do_lift_1 constName)

unsafe def Lean.evalConstCheck {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] [Lean.MonadOptions m] (α : Type) (typeName : Lake.Name) (constName : Lake.Name) : m α

Equations

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

def Lean.findModuleOf? {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] (declName : Lake.Name) : m (Option Lake.Name)

Equations

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

def Lean.isEnumType {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] (declName : Lake.Name) : m Bool

Equations

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