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 |