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.isInductiveCore? (env : Environment) (declName : Name) : Option InductiveVal

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

def Lean.isDefn? {m : Type → Type} [Monad m] [MonadEnv m] (constName : Name) : m (Option DefinitionVal)

def Lean.isCtor? {m : Type → Type} [Monad m] [MonadEnv m] (constName : Name) : m (Option ConstructorVal)

def Lean.isRec? {m : Type → Type} [Monad m] [MonadEnv m] (constName : Name) : m (Option RecursorVal)

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.matchConstNonRecStructure for a more restrictive version.

@[inline]

def Lean.matchConstNonRecStructure {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 a non-recursive inductive type with no indices and with one constructor. Such a type satisfies Lean.isNonRecStructure. See also Lean.matchConstStructure for a less restrictive version.

@[extern lean_has_compile_error]

opaque Lean.hasCompileError (env : Environment) (constName : Name) : Bool

unsafe def Lean.evalConst {m : Type → Type} [Monad m] [MonadEnv m] [MonadError m] [MonadOptions m] (α : Type) (constName : Name) (checkMeta : Bool := true) : 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.isLargeEliminating {m : Type → Type} [Monad m] [MonadEnv m] [MonadError m] (declName : Name) : m Bool

Returns true if the recursor of the inductive type declName eliminates into an arbitrary Sort, which is the case exactly when it takes an extra universe parameter for the motive.

Constructions that turn a value of the type into data (T.ctorIdx, T._sizeOf_1, T.noConfusion, …) are only possible for such types.

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