| :< | Language.Lean.List, Language.Lean |
| <| | Language.Lean.List, Language.Lean |
| addInductiveDecl | Language.Lean.Inductive |
| AnonymousName | Language.Lean.Internal.Name, Language.Lean.Name, Language.Lean |
| anonymousName | Language.Lean.Internal.Name, Language.Lean.Name, Language.Lean |
| appExpr | Language.Lean.Expr, Language.Lean |
| Axiom | Language.Lean.Decl, Language.Lean |
| axiom | Language.Lean.Decl, Language.Lean |
| BinderDefault | Language.Lean.Internal.Expr, Language.Lean.Expr, Language.Lean |
| BinderHidden | Language.Lean.Internal.Expr, Language.Lean.Expr, Language.Lean |
| BinderImplicit | Language.Lean.Internal.Expr, Language.Lean.Expr, Language.Lean |
| BinderInstImplicit | Language.Lean.Internal.Expr, Language.Lean.Expr, Language.Lean |
| BinderKind | Language.Lean.Internal.Expr, Language.Lean.Expr, Language.Lean |
| BinderStrictImplicit | Language.Lean.Internal.Expr, Language.Lean.Expr, Language.Lean |
| boolOption | Language.Lean.Options, Language.Lean |
| Buffered | Language.Lean.Internal.IOS, Language.Lean.IOS, Language.Lean |
| BufferedIOState | Language.Lean.Internal.IOS |
| BufferedRepr | Language.Lean.IOS, Language.Lean |
| CertDecl | Language.Lean.Internal.Decl, Language.Lean.Decl, Language.Lean |
| CertDeclPtr | Language.Lean.Internal.Decl |
| check | Language.Lean.Decl, Language.Lean |
| checkType | Language.Lean.Typechecker, Language.Lean |
| concatList | Language.Lean.List, Language.Lean |
| Constant | Language.Lean.Decl, Language.Lean |
| constant | Language.Lean.Decl, Language.Lean |
| constExpr | Language.Lean.Expr, Language.Lean |
| ConstraintSeq | Language.Lean.Internal.Typechecker, Language.Lean.Typechecker, Language.Lean |
| ConstraintSeqPtr | Language.Lean.Internal.Typechecker |
| containsOption | Language.Lean.Options, Language.Lean |
| Decl | Language.Lean.Internal.Decl, Language.Lean.Decl, Language.Lean |
| declName | Language.Lean.Decl, Language.Lean |
| DeclPtr | Language.Lean.Internal.Decl |
| declType | Language.Lean.Decl, Language.Lean |
| declUnivParams | Language.Lean.Decl, Language.Lean |
| DeclView | Language.Lean.Decl, Language.Lean |
| declView | Language.Lean.Decl, Language.Lean |
| decodeLeanString | Language.Lean.Internal.String |
| Definition | Language.Lean.Decl, Language.Lean |
| definition | Language.Lean.Decl, Language.Lean |
| definitionWith | Language.Lean.Decl, Language.Lean |
| doubleOption | Language.Lean.Options, Language.Lean |
| emptyOptions | Language.Lean.Internal.Options, Language.Lean.Options, Language.Lean |
| Env | |
| 1 (Type/Class) | Language.Lean.Internal.Decl, Language.Lean.Env, Language.Lean.Decl, Language.Lean |
| 2 (Data Constructor) | Language.Lean.Internal.Decl, Language.Lean.Decl, Language.Lean |
| envAddDecl | Language.Lean.Env, Language.Lean |
| envAddUniv | Language.Lean.Env, Language.Lean |
| envContainsDecl | Language.Lean.Env, Language.Lean |
| envContainsProofIrrelProp | Language.Lean.Env, Language.Lean |
| envContainsUniv | Language.Lean.Env, Language.Lean |
| envDecls | Language.Lean.Env, Language.Lean |
| envExport | Language.Lean.Module, Language.Lean |
| envForget | Language.Lean.Env, Language.Lean |
| envImport | Language.Lean.Module, Language.Lean |
| envIsDescendant | Language.Lean.Env, Language.Lean |
| envIsImpredicative | Language.Lean.Env, Language.Lean |
| envLookupDecl | Language.Lean.Env, Language.Lean |
| EnvPtr | Language.Lean.Internal.Decl |
| envReplaceAxiom | Language.Lean.Env, Language.Lean |
| envTrustLevel | Language.Lean.Env, Language.Lean |
| envUnivs | Language.Lean.Env, Language.Lean |
| ExceptionPtr | Language.Lean.Internal.Exception |
| explicitUniv | Language.Lean.Univ, Language.Lean |
| Expr | Language.Lean.Internal.Expr, Language.Lean.Expr, Language.Lean |
| ExprApp | Language.Lean.Expr, Language.Lean |
| ExprConst | Language.Lean.Expr, Language.Lean |
| ExprLambda | Language.Lean.Expr, Language.Lean |
| ExprLocal | Language.Lean.Expr, Language.Lean |
| exprLt | Language.Lean.Internal.Expr, Language.Lean.Expr, Language.Lean |
| ExprMacro | Language.Lean.Expr, Language.Lean |
| ExprMeta | Language.Lean.Expr, Language.Lean |
| ExprPi | Language.Lean.Expr, Language.Lean |
| ExprPtr | Language.Lean.Internal.Expr |
| ExprSort | Language.Lean.Expr, Language.Lean |
| exprToString | Language.Lean.Internal.Expr, Language.Lean.Expr, Language.Lean |
| ExprVar | Language.Lean.Expr, Language.Lean |
| ExprView | Language.Lean.Expr, Language.Lean |
| exprView | Language.Lean.Expr, Language.Lean |
| forEnvDecl_ | Language.Lean.Env, Language.Lean |
| forEnvUniv_ | Language.Lean.Env, Language.Lean |
| fromList | Language.Lean.List, Language.Lean |
| fromListDefault | Language.Lean.List, Language.Lean |
| fromListN | Language.Lean.List, Language.Lean |
| getDiagnosticOutput | Language.Lean.IOS, Language.Lean |
| getLeanString | Language.Lean.Internal.String |
| getRegularOutput | Language.Lean.IOS, Language.Lean |
| getStateOptions | Language.Lean.IOS, Language.Lean |
| globalUniv | Language.Lean.Univ, Language.Lean |
| hottEnv | Language.Lean.Env, Language.Lean |
| hottPath | Language.Lean.Module, Language.Lean |
| imaxUniv | Language.Lean.Univ, Language.Lean |
| IndexName | Language.Lean.Internal.Name, Language.Lean.Name, Language.Lean |
| InductiveDecl | Language.Lean.Internal.Inductive, Language.Lean.Inductive |
| inductiveDecl | Language.Lean.Inductive |
| inductiveDeclNumParams | Language.Lean.Inductive |
| InductiveDeclPtr | Language.Lean.Internal.Inductive |
| inductiveDeclTypes | Language.Lean.Inductive |
| inductiveDeclUnivParams | Language.Lean.Inductive |
| InductiveType | Language.Lean.Internal.Inductive, Language.Lean.Inductive |
| inductiveType | Language.Lean.Inductive |
| inductiveTypeConstructors | Language.Lean.Inductive |
| inductiveTypeHasDepElim | Language.Lean.Inductive |
| inductiveTypeName | Language.Lean.Inductive |
| InductiveTypePtr | Language.Lean.Internal.Inductive |
| inductiveTypeType | Language.Lean.Inductive |
| inferType | Language.Lean.Typechecker, Language.Lean |
| instantiateUniv | Language.Lean.Univ, Language.Lean |
| instantiateUniv2 | Language.Lean.Univ, Language.Lean |
| intOption | Language.Lean.Options, Language.Lean |
| IOState | Language.Lean.Internal.IOS, Language.Lean.IOS, Language.Lean |
| IOStateType | Language.Lean.Internal.IOS, Language.Lean.IOS, Language.Lean |
| IOStateTypeRepr | Language.Lean.IOS, Language.Lean |
| isDefEq | Language.Lean.Typechecker, Language.Lean |
| IsLeanValue | Language.Lean.Internal.Exception |
| IsList | Language.Lean.List, Language.Lean |
| IsListIso | Language.Lean.List, Language.Lean |
| Item | Language.Lean.List, Language.Lean |
| joinOptions | Language.Lean.Internal.Options, Language.Lean.Options, Language.Lean |
| 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 |
| MacroDef | Language.Lean.Internal.Expr, Language.Lean.Expr, Language.Lean |
| MacroDefPtr | Language.Lean.Internal.Expr |
| macroExpr | Language.Lean.Expr, Language.Lean |
| mapList | Language.Lean.List, Language.Lean |
| maxUniv | Language.Lean.Univ, Language.Lean |
| metaUniv | Language.Lean.Univ, Language.Lean |
| metavarExpr | Language.Lean.Expr, Language.Lean |
| mkBufferedIOState | Language.Lean.IOS, Language.Lean |
| mkBufferedIOStateWithOptions | Language.Lean.IOS, Language.Lean |
| mkLeanString | Language.Lean.Internal.String |
| mkLeanText | Language.Lean.Internal.String |
| mkLeanValue | Language.Lean.Internal.Exception |
| mkStandardIOState | Language.Lean.IOS, Language.Lean |
| mkStandardIOStateWithOptions | Language.Lean.IOS, Language.Lean |
| Name | Language.Lean.Internal.Name, Language.Lean.Name, Language.Lean |
| nameAppend | Language.Lean.Internal.Name, Language.Lean.Name, Language.Lean |
| nameAppendIndex | Language.Lean.Internal.Name, Language.Lean.Name, Language.Lean |
| NamePtr | Language.Lean.Internal.Name |
| nameToString | Language.Lean.Internal.Name, Language.Lean.Name, Language.Lean |
| NameView | Language.Lean.Internal.Name, Language.Lean.Name, Language.Lean |
| nameView | Language.Lean.Internal.Name, Language.Lean.Name, Language.Lean |
| Nil | Language.Lean.List, Language.Lean |
| nil | Language.Lean.List, Language.Lean |
| normalizeUniv | Language.Lean.Univ, Language.Lean |
| nullOptions | Language.Lean.Options, Language.Lean |
| Options | Language.Lean.Internal.Options, Language.Lean.Options, Language.Lean |
| OptionsPtr | Language.Lean.Internal.Options |
| OutCertDeclPtr | Language.Lean.Internal.Decl |
| OutConstraintSeqPtr | Language.Lean.Internal.Typechecker |
| OutDeclPtr | Language.Lean.Internal.Decl |
| OutEnvPtr | Language.Lean.Internal.Decl |
| OutExceptionPtr | Language.Lean.Internal.Exception |
| OutExprPtr | Language.Lean.Internal.Expr |
| OutInductiveDeclPtr | Language.Lean.Internal.Inductive |
| OutInductiveTypePtr | Language.Lean.Internal.Inductive |
| OutListExprPtr | Language.Lean.Internal.Expr |
| OutListInductiveTypePtr | Language.Lean.Internal.Inductive |
| OutListNamePtr | Language.Lean.Internal.Name |
| OutListUnivPtr | Language.Lean.Internal.Univ |
| OutMacroDefPtr | Language.Lean.Internal.Expr |
| OutNamePtr | Language.Lean.Internal.Name |
| OutOptionsPtr | Language.Lean.Internal.Options |
| OutSomeIOStatePtr | Language.Lean.Internal.IOS |
| OutTypecheckerPtr | Language.Lean.Internal.Typechecker |
| OutUnivPtr | Language.Lean.Internal.Univ |
| paramUniv | Language.Lean.Univ, Language.Lean |
| piExpr | Language.Lean.Expr, Language.Lean |
| ppExpr | Language.Lean.IOS, Language.Lean |
| recursorName | Language.Lean.Inductive |
| resetDiagnosticOutput | Language.Lean.IOS, Language.Lean |
| resetRegularOutput | Language.Lean.IOS, Language.Lean |
| runLeanMaybeFn | Language.Lean.Internal.Exception |
| runLeanPartialAction | Language.Lean.Internal.Exception |
| runLeanPartialFn | Language.Lean.Internal.Exception |
| setStateOptions | Language.Lean.IOS, Language.Lean |
| showUniv | Language.Lean.Internal.Univ, Language.Lean.Univ, Language.Lean |
| showUnivUsing | Language.Lean.Internal.Univ, Language.Lean.Univ, Language.Lean |
| someIOS | Language.Lean.Internal.IOS |
| SomeIOState | Language.Lean.Internal.IOS |
| SomeIOStatePtr | Language.Lean.Internal.IOS |
| sortExpr | Language.Lean.Expr, Language.Lean |
| Standard | Language.Lean.Internal.IOS, Language.Lean.IOS, Language.Lean |
| standardEnv | Language.Lean.Env, Language.Lean |
| StandardRepr | Language.Lean.IOS, Language.Lean |
| stateTypeRepr | Language.Lean.IOS, Language.Lean |
| stdPath | Language.Lean.Module, Language.Lean |
| StringName | Language.Lean.Internal.Name, Language.Lean.Name, Language.Lean |
| stringOption | Language.Lean.Options, Language.Lean |
| succUniv | Language.Lean.Univ, Language.Lean |
| Theorem | Language.Lean.Decl, Language.Lean |
| theorem | Language.Lean.Decl, Language.Lean |
| theoremWith | Language.Lean.Decl, Language.Lean |
| throwLeanException | Language.Lean.Internal.Exception |
| toList | Language.Lean.List, Language.Lean |
| traverseList | Language.Lean.List, Language.Lean |
| trustHigh | Language.Lean.Env, Language.Lean |
| TrustLevel | Language.Lean.Env, Language.Lean |
| tryAllocLeanValue | Language.Lean.Internal.Exception |
| tryGetEnum | Language.Lean.Internal.Exception.Unsafe |
| tryGetLeanMaybeValue | Language.Lean.Internal.Exception.Unsafe |
| tryGetLeanValue | Language.Lean.Internal.Exception.Unsafe |
| Typechecker | Language.Lean.Internal.Typechecker, Language.Lean.Typechecker, Language.Lean |
| typechecker | Language.Lean.Typechecker, Language.Lean |
| TypecheckerPtr | Language.Lean.Internal.Typechecker |
| uintOption | Language.Lean.Options, Language.Lean |
| Univ | Language.Lean.Internal.Univ, Language.Lean.Univ, Language.Lean |
| univGeq | Language.Lean.Univ, Language.Lean |
| UnivGlobal | Language.Lean.Univ, Language.Lean |
| UnivIMax | Language.Lean.Univ, Language.Lean |
| univLt | Language.Lean.Internal.Univ, Language.Lean.Univ, Language.Lean |
| UnivMax | Language.Lean.Univ, Language.Lean |
| UnivMeta | Language.Lean.Univ, Language.Lean |
| UnivParam | Language.Lean.Univ, Language.Lean |
| UnivPtr | Language.Lean.Internal.Univ |
| UnivSucc | Language.Lean.Univ, Language.Lean |
| UnivView | Language.Lean.Univ, Language.Lean |
| univView | Language.Lean.Univ, Language.Lean |
| UnivZero | Language.Lean.Univ, Language.Lean |
| varExpr | Language.Lean.Expr, Language.Lean |
| whnf | Language.Lean.Typechecker, Language.Lean |
| withBufferedIOState | Language.Lean.Internal.IOS |
| withCertDecl | Language.Lean.Internal.Decl |
| withConstraintSeq | Language.Lean.Internal.Typechecker |
| withDecl | Language.Lean.Internal.Decl |
| withEnv | Language.Lean.Internal.Decl |
| withExpr | Language.Lean.Internal.Expr |
| withInductiveDecl | Language.Lean.Internal.Inductive |
| withInductiveType | Language.Lean.Internal.Inductive |
| withIOState | Language.Lean.Internal.IOS |
| withLeanStringPtr | Language.Lean.Internal.String |
| withLeanTextPtr | Language.Lean.Internal.String |
| withListExpr | Language.Lean.Internal.Expr |
| withListInductiveType | Language.Lean.Internal.Inductive |
| withListName | Language.Lean.Internal.Name |
| withListUniv | Language.Lean.Internal.Univ |
| withMacroDef | Language.Lean.Internal.Expr |
| withName | Language.Lean.Internal.Name |
| withOptions | Language.Lean.Internal.Options |
| withSomeIOState | Language.Lean.Internal.IOS |
| withTypechecker | Language.Lean.Internal.Typechecker |
| withUniv | Language.Lean.Internal.Univ |
| zeroUniv | Language.Lean.Univ, Language.Lean |