Instances For
def
Lean.withEnv
{m : Type → Type}
{α : Type}
[Monad m]
[MonadFinally m]
[Lean.MonadEnv m]
(env : Lean.Environment)
(x : m α)
:
m α
Instances For
Instances For
Instances For
@[inline]
def
Lean.withoutModifyingEnv
{m : Type → Type}
[Monad m]
[Lean.MonadEnv m]
[MonadFinally m]
{α : Type}
(x : m α)
:
m α
Instances For
@[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
Instances For
@[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 α
Instances For
@[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 α
Instances For
@[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 α
Instances For
@[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 α
Instances For
Instances For
def
Lean.mkAuxName
{m : Type → Type}
[Monad m]
[Lean.MonadEnv m]
(baseName : Lake.Name)
(idx : Nat)
:
Instances For
def
Lean.getConstInfo
{m : Type → Type}
[Monad m]
[Lean.MonadEnv m]
[Lean.MonadError m]
(constName : Lake.Name)
:
Instances For
def
Lean.mkConstWithLevelParams
{m : Type → Type}
[Monad m]
[Lean.MonadEnv m]
[Lean.MonadError m]
(constName : Lake.Name)
:
Instances For
def
Lean.getConstInfoDefn
{m : Type → Type}
[Monad m]
[Lean.MonadEnv m]
[Lean.MonadError m]
(constName : Lake.Name)
:
Instances For
def
Lean.getConstInfoInduct
{m : Type → Type}
[Monad m]
[Lean.MonadEnv m]
[Lean.MonadError m]
(constName : Lake.Name)
:
Instances For
def
Lean.getConstInfoCtor
{m : Type → Type}
[Monad m]
[Lean.MonadEnv m]
[Lean.MonadError m]
(constName : Lake.Name)
:
Instances For
def
Lean.getConstInfoRec
{m : Type → Type}
[Monad m]
[Lean.MonadEnv m]
[Lean.MonadError m]
(constName : Lake.Name)
:
Instances For
@[inline]
def
Lean.matchConstStruct
{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 α
Instances For
unsafe def
Lean.evalConst
{m : Type → Type}
[Monad m]
[Lean.MonadEnv m]
[Lean.MonadError m]
[Lean.MonadOptions m]
(α : Type)
(constName : Lake.Name)
:
m α
Instances For
unsafe def
Lean.evalConstCheck
{m : Type → Type}
[Monad m]
[Lean.MonadEnv m]
[Lean.MonadError m]
[Lean.MonadOptions m]
(α : Type)
(typeName : Lake.Name)
(constName : Lake.Name)
:
m α
Instances For
def
Lean.findModuleOf?
{m : Type → Type}
[Monad m]
[Lean.MonadEnv m]
[Lean.MonadError m]
(declName : Lake.Name)
:
Instances For
def
Lean.isEnumType
{m : Type → Type}
[Monad m]
[Lean.MonadEnv m]
[Lean.MonadError m]
(declName : Lake.Name)
:
m Bool