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

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

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

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

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

@[inline]

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

@[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

@[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 α

@[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 α

@[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 α

@[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 α

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

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

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

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

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

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

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

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

@[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 α

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

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 α

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

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