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
- One or more equations did not get rendered due to their size.
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 __do_lift ← Lean.getEnv pure (Lean.isRecCore __do_lift 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 __do_lift ← Lean.getEnv pure (Lean.Environment.contains __do_lift 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 __do_lift ← Lean.getEnv pure (Lean.mkAuxNameAux __do_lift 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.getConstInfoDefn
{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.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.
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 __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}
[inst : Monad m]
[inst : Lean.MonadEnv m]
[inst : Lean.MonadError m]
[inst : Lean.MonadOptions m]
(α : Type)
(typeName : Lean.Name)
(constName : Lean.Name)
:
m α
Equations
- One or more equations did not get rendered due to their size.
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.