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.mkAuxName {m : Type → Type} [Monad m] [MonadEnv m] (baseName : Name) (idx : Nat) : m 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] [MonadEnv m] [MonadError m] (constName : Name) : m ConstantInfo

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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