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

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

def Lean.isInductiveCore (env : Environment) (declName : Name) : Bool

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

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

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

@[inline]

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

@[inline]

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

Similar to withoutModifyingEnv, but also returns the updated environment

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

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

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

def Lean.getConstVal {m : Type → Type} [Monad m] [MonadEnv m] [MonadError m] (constName : Name) : m ConstantVal

def Lean.getAsyncConstInfo {m : Type → Type} [Monad m] [MonadEnv m] [MonadError m] (constName : Name) (skipRealize : Bool := false) : m AsyncConstantInfo

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

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

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

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

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

@[inline]

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

Matches if e is a constant that is an inductive type with one constructor. Such types can be used with primitive projections. See also Lean.matchConstStructLike for a more restrictive version.

@[inline]

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

Matches if e is a constant that is an non-recursive inductive type with no indices and with one constructor. Such a type satisfies Lean.isStructureLike. See also Lean.matchConstStructure for a less restrictive version.

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

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

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

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