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 α

Equations

• Lean.withEnv env x = do let saved ← Lean.getEnv tryFinally (do Lean.setEnv env x) (Lean.setEnv saved)

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

Equations

• Lean.isInductive declName = do let __do_lift ← Lean.getEnv match __do_lift.find? declName with | some (Lean.ConstantInfo.inductInfo val) => pure true | x => pure false

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

Equations

• Lean.isRecCore env declName = match env.find? declName with | some (Lean.ConstantInfo.recInfo val) => true | x => false

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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

Equations

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

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

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

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

@[inline]

def Lean.matchConstStructure {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 α

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] [Lean.MonadEnv m] [Lean.MonadError m] (e : Lean.Expr) (failK : Unit → m α) (k : Lean.InductiveVal → List Lean.Level → Lean.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] [Lean.MonadEnv m] [Lean.MonadError m] [Lean.MonadOptions m] (α : Type) (constName : Lean.Name) : m α

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

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

Equations

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

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