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

Equations

• Lean.setEnv env = Lean.modifyEnv fun (x : Lean.Environment) => env

def Lean.withEnv {m : Type → Type} {α : Type} [Monad m] [MonadFinally m] [MonadEnv m] (env : 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.isInductiveCore (env : Environment) (declName : Name) : Bool

Equations

• Lean.isInductiveCore env declName = match env.findAsync? declName with | some { name := name, kind := Lean.ConstantKind.induct, sig := sig, constInfo := constInfo } => true | x => false

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

Equations

• Lean.isInductive declName = do let __do_lift ← Lean.getEnv pure (Lean.isInductiveCore __do_lift declName)

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

Equations

• Lean.isRecCore env declName = match env.findAsync? declName with | some { name := name, kind := Lean.ConstantKind.recursor, sig := sig, constInfo := constInfo } => true | x => false

def Lean.isRec {m : Type → Type} [Monad m] [MonadEnv m] (declName : 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] [MonadEnv m] [MonadFinally m] {α : Type} (x : m α) : m α

Equations

• Lean.withoutModifyingEnv x = do let __do_lift ← Lean.getEnv Lean.withEnv __do_lift.unlockAsync x

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

Equations

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

@[inline]

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

Equations

• Lean.matchConst (Lean.Expr.const constName us) failK k = do let __do_lift ← Lean.getEnv match __do_lift.find? constName with | some cinfo => k cinfo us | none => failK ()
• Lean.matchConst e failK k = failK ()

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

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

Equations

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

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

Equations

• Lean.getConstInfo constName = do let __do_lift ← Lean.getEnv match __do_lift.find? constName with | some info => pure info | none => Lean.throwUnknownConstant constName

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

Equations

• Lean.getConstVal constName = do let __do_lift ← Lean.getEnv match __do_lift.findConstVal? constName with | some val => pure val | none => Lean.throwUnknownConstant constName

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

Equations

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

def Lean.isInductiveCore? (env : Environment) (declName : Name) : Option InductiveVal

Equations

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

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

Equations

• Lean.isInductive? declName = do let __do_lift ← Lean.getEnv pure (Lean.isInductiveCore? __do_lift declName)

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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.

Equations

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

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

Equations

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