lambdaExpr | Language.Lean.Expr, Language.Lean |
LeanException | |
1 (Type/Class) | Language.Lean.Internal.Exception, Language.Lean.Exception, Language.Lean |
2 (Data Constructor) | Language.Lean.Internal.Exception, Language.Lean.Exception, Language.Lean |
LeanExceptionKind | Language.Lean.Internal.Exception, Language.Lean.Exception, Language.Lean |
leanExceptionKind | Language.Lean.Internal.Exception, Language.Lean.Exception, Language.Lean |
leanExceptionName | Language.Lean.Internal.Exception, Language.Lean.Exception, Language.Lean |
LeanInterrupted | Language.Lean.Internal.Exception, Language.Lean.Exception, Language.Lean |
LeanKernelException | Language.Lean.Internal.Exception, Language.Lean.Exception, Language.Lean |
leanKernelException | Language.Lean.Internal.Exception |
LeanOtherException | Language.Lean.Internal.Exception, Language.Lean.Exception, Language.Lean |
leanOtherException | Language.Lean.Internal.Exception |
LeanOutOfMemory | Language.Lean.Internal.Exception, Language.Lean.Exception, Language.Lean |
LeanPartialAction | Language.Lean.Internal.Exception |
LeanPartialFn | Language.Lean.Internal.Exception |
LeanSystemException | Language.Lean.Internal.Exception, Language.Lean.Exception, Language.Lean |
List | Language.Lean.List, Language.Lean |
ListExpr | Language.Lean.Internal.Expr |
ListExprPtr | Language.Lean.Internal.Expr |
ListInductiveType | Language.Lean.Internal.Inductive |
ListInductiveTypePtr | Language.Lean.Internal.Inductive |
ListName | Language.Lean.Internal.Name |
ListNamePtr | Language.Lean.Internal.Name |
ListUniv | Language.Lean.Internal.Univ |
ListUnivPtr | Language.Lean.Internal.Univ |
ListView | Language.Lean.List, Language.Lean |
listView | Language.Lean.List, Language.Lean |
localExpr | Language.Lean.Expr, Language.Lean |
localExtExpr | Language.Lean.Expr, Language.Lean |
lookupConstructorInductiveTypeName | Language.Lean.Inductive |
lookupInductiveDecl | Language.Lean.Inductive |
lookupInductiveTypeNumIndices | Language.Lean.Inductive |
lookupInductiveTypeNumMinorPremises | Language.Lean.Inductive |
lookupRecursorInductiveTypeName | Language.Lean.Inductive |