Equations
- Lean.setEnv env = Lean.modifyEnv fun x => env
def
Lean.withEnv
{m : Type → Type}
{α : Type}
[inst : Monad m]
[inst : MonadFinally m]
[inst : 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}
[inst : Monad m]
[inst : Lean.MonadEnv m]
(declName : Lean.Name)
:
m Bool
Equations
- Lean.isInductive declName = do let a ← Lean.getEnv match Lean.Environment.find? a declName with | some (Lean.ConstantInfo.inductInfo val) => pure true | x => pure false
Equations
- Lean.isRecCore env declName = match Lean.Environment.find? env declName with | some (Lean.ConstantInfo.recInfo val) => true | x => false
def
Lean.isRec
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadEnv m]
(declName : Lean.Name)
:
m Bool
Equations
- Lean.isRec declName = do let a ← Lean.getEnv pure (Lean.isRecCore a declName)
@[inline]
def
Lean.withoutModifyingEnv
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadEnv m]
[inst : MonadFinally m]
{α : Type}
(x : m α)
:
m α
Equations
- Lean.withoutModifyingEnv x = do let env ← Lean.getEnv tryFinally x (Lean.setEnv env)
@[inline]
def
Lean.withoutModifyingEnv'
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadEnv m]
[inst : 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}
[inst : Monad m]
[inst : Lean.MonadEnv m]
(e : Lean.Expr)
(failK : Unit → m α)
(k : Lean.ConstantInfo → List Lean.Level → m α)
:
m α
Equations
- One or more equations did not get rendered due to their size.
@[inline]
def
Lean.matchConstInduct
{m : Type → Type}
{α : Type}
[inst : Monad m]
[inst : Lean.MonadEnv m]
(e : Lean.Expr)
(failK : Unit → m α)
(k : Lean.InductiveVal → List Lean.Level → m α)
:
m α
Equations
- Lean.matchConstInduct e failK k = Lean.matchConst e failK fun cinfo us => match cinfo with | Lean.ConstantInfo.inductInfo val => k val us | x => failK ()
@[inline]
def
Lean.matchConstCtor
{m : Type → Type}
{α : Type}
[inst : Monad m]
[inst : Lean.MonadEnv m]
(e : Lean.Expr)
(failK : Unit → m α)
(k : Lean.ConstructorVal → List Lean.Level → m α)
:
m α
Equations
- Lean.matchConstCtor e failK k = Lean.matchConst e failK fun cinfo us => match cinfo with | Lean.ConstantInfo.ctorInfo val => k val us | x => failK ()
@[inline]
def
Lean.matchConstRec
{m : Type → Type}
{α : Type}
[inst : Monad m]
[inst : Lean.MonadEnv m]
(e : Lean.Expr)
(failK : Unit → m α)
(k : Lean.RecursorVal → List Lean.Level → m α)
:
m α
Equations
- Lean.matchConstRec e failK k = Lean.matchConst e failK fun cinfo us => match cinfo with | Lean.ConstantInfo.recInfo val => k val us | x => failK ()
def
Lean.hasConst
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadEnv m]
(constName : Lean.Name)
:
m Bool
Equations
- Lean.hasConst constName = do let a ← Lean.getEnv pure (Lean.Environment.contains a constName)
def
Lean.mkAuxName
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadEnv m]
(baseName : Lean.Name)
(idx : Nat)
:
Equations
- Lean.mkAuxName baseName idx = do let a ← Lean.getEnv pure (Lean.mkAuxNameAux a baseName idx)
def
Lean.getConstInfo
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadEnv m]
[inst : Lean.MonadError m]
(constName : Lean.Name)
:
Equations
- One or more equations did not get rendered due to their size.
def
Lean.mkConstWithLevelParams
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadEnv m]
[inst : Lean.MonadError m]
(constName : Lean.Name)
:
Equations
- Lean.mkConstWithLevelParams constName = do let info ← Lean.getConstInfo constName pure (Lean.mkConst constName (List.map Lean.mkLevelParam (Lean.ConstantInfo.levelParams info)))
def
Lean.getConstInfoInduct
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadEnv m]
[inst : Lean.MonadError m]
(constName : Lean.Name)
:
Equations
- One or more equations did not get rendered due to their size.
def
Lean.getConstInfoCtor
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadEnv m]
[inst : Lean.MonadError m]
(constName : Lean.Name)
:
Equations
- One or more equations did not get rendered due to their size.
def
Lean.getConstInfoRec
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadEnv m]
[inst : Lean.MonadError m]
(constName : Lean.Name)
:
Equations
- One or more equations did not get rendered due to their size.
@[inline]
def
Lean.matchConstStruct
{m : Type → Type}
{α : Type}
[inst : Monad m]
[inst : Lean.MonadEnv m]
[inst : Lean.MonadError m]
(e : Lean.Expr)
(failK : Unit → m α)
(k : Lean.InductiveVal → List Lean.Level → Lean.ConstructorVal → m α)
:
m α
Equations
- One or more equations did not get rendered due to their size.
def
Lean.addDecl
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadEnv m]
[inst : Lean.MonadError m]
[inst : Lean.MonadOptions m]
[inst : Lean.MonadLog m]
[inst : Lean.AddMessageContext m]
(decl : Lean.Declaration)
:
m Unit
Equations
- One or more equations did not get rendered due to their size.
def
Lean.compileDecl
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadEnv m]
[inst : Lean.MonadError m]
[inst : Lean.MonadOptions m]
(decl : Lean.Declaration)
:
m Unit
Equations
- One or more equations did not get rendered due to their size.
def
Lean.addAndCompile
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadEnv m]
[inst : Lean.MonadError m]
[inst : Lean.MonadOptions m]
[inst : Lean.MonadLog m]
[inst : Lean.AddMessageContext m]
(decl : Lean.Declaration)
:
m Unit
Equations
- Lean.addAndCompile decl = do Lean.addDecl decl Lean.compileDecl decl
unsafe def
Lean.evalConst
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadEnv m]
[inst : Lean.MonadError m]
[inst : Lean.MonadOptions m]
(α : Type)
(constName : Lean.Name)
:
m α
Equations
- Lean.evalConst α constName = do let a ← Lean.getEnv let a_1 ← Lean.getOptions Lean.ofExcept (Lean.Environment.evalConst α a a_1 constName)
unsafe def
Lean.evalConstCheck
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadEnv m]
[inst : Lean.MonadError m]
[inst : Lean.MonadOptions m]
(α : Type)
(typeName : Lean.Name)
(constName : Lean.Name)
:
m α
Equations
- Lean.evalConstCheck α typeName constName = do let a ← Lean.getEnv let a_1 ← Lean.getOptions Lean.ofExcept (Lean.Environment.evalConstCheck α a a_1 typeName constName)
def
Lean.findModuleOf?
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadEnv m]
[inst : Lean.MonadError m]
(declName : Lean.Name)
:
Equations
- One or more equations did not get rendered due to their size.
def
Lean.isEnumType
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadEnv m]
[inst : Lean.MonadError m]
(declName : Lean.Name)
:
m Bool
Equations
- One or more equations did not get rendered due to their size.