EAll | Idris.AbsSyntaxTree, Idris.AbsSyntax |
EDefns | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Edit | Idris.AbsSyntaxTree, Idris.AbsSyntax |
edit | Idris.REPL |
eEVAL | IRTS.Defunctionalise |
EInfo | Idris.AbsSyntaxTree, Idris.AbsSyntax |
eInfoNames | Idris.AbsSyntaxTree, Idris.AbsSyntax |
EitherErr | Idris.AbsSyntax |
Elab | Idris.Core.Elaborate |
elab | Idris.ElabTerm |
Elab' | Idris.Core.Elaborate |
elabCaseBlock | Idris.Elab.Utils |
elabClass | Idris.Elab.Class |
elabClause | Idris.Elab.Clause |
elabClauses | Idris.Elab.Clause |
ElabCtxt | |
1 (Type/Class) | Idris.ElabTerm |
2 (Data Constructor) | Idris.ElabTerm |
ElabD | Idris.AbsSyntaxTree, Idris.AbsSyntax |
elabData | Idris.Elab.Data |
ElabDebug | Idris.Core.TT |
elabDecl | Idris.ElabDecls |
elabDecl' | Idris.ElabDecls |
elabDecls | Idris.ElabDecls |
elabDocTerms | Idris.Elab.Value |
elabFC | Idris.AbsSyntaxTree, Idris.AbsSyntax |
ElabInfo | Idris.AbsSyntaxTree, Idris.AbsSyntax |
elabInstance | Idris.Elab.Instance |
elabMain | Idris.ElabDecls |
ElabMode | Idris.ElabTerm |
elaborate | Idris.Core.Elaborate |
Elaborating | Idris.Core.TT |
ElaboratingArg | Idris.Core.TT |
elaboratingArgErr | Idris.ElabTerm |
elaborating_app | Idris.Core.Elaborate |
elabPE | Idris.Elab.Clause |
elabPostulate | Idris.Elab.Type |
elabPrims | Idris.ElabDecls |
elabProvider | Idris.Elab.Provider |
elabRecord | Idris.Elab.Record |
ElabResult | |
1 (Type/Class) | Idris.ElabTerm |
2 (Data Constructor) | Idris.ElabTerm |
ElabState | Idris.Core.Elaborate |
elabStep | Idris.Prover |
elabTransform | Idris.Elab.Transform |
elabType | Idris.Elab.Type |
elabType' | Idris.Elab.Type |
elabVal | Idris.Elab.Value |
elabValBind | Idris.Elab.Value |
ElabWhat | Idris.AbsSyntaxTree, Idris.AbsSyntax |
elab_stack | Idris.AbsSyntaxTree, Idris.AbsSyntax |
ELHS | Idris.ElabTerm |
ElimN | Idris.Core.TT |
elog | Idris.Core.Elaborate |
Emph | Idris.Docstrings |
emptyContext | Idris.Core.TT |
emptyDocstring | Idris.Docstrings |
emptyFC | Idris.Core.TT |
EmptyMI | Idris.Core.Evaluate |
emptySyntaxRules | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Endianness | IRTS.Lang, IRTS.Defunctionalise |
EndUnify | Idris.Core.ProofState, Idris.Core.Elaborate |
end_unify | Idris.Core.Elaborate |
Entity | Idris.Docstrings |
Env | Idris.Core.TT |
envAtFocus | Idris.Core.ProofState, Idris.Core.Elaborate |
environment | IRTS.CodegenCommon |
envlen | Idris.Core.TT |
EnvTT | Idris.Core.TT |
envTupleType | Idris.ElabTerm |
eol | Idris.ParseHelpers, Idris.Parser |
eqCon | Idris.AbsSyntaxTree, Idris.AbsSyntax |
eqDecl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
eqDoc | Idris.AbsSyntaxTree, Idris.AbsSyntax |
eqOpts | Idris.AbsSyntaxTree, Idris.AbsSyntax |
eqParamDoc | Idris.AbsSyntaxTree, Idris.AbsSyntax |
eqProp | Idris.ParseHelpers, Idris.Parser |
eqTy | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Equiv | |
1 (Data Constructor) | Idris.Core.ProofState, Idris.Core.Elaborate |
2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
equiv | Idris.Core.Elaborate |
Erased | Idris.Core.TT |
ErasureInfo | Idris.Core.CaseTree |
ERHS | Idris.ElabTerm |
Err | Idris.Core.TT |
Err' | Idris.Core.TT |
errAt | Idris.Core.Elaborate |
ErrContext | |
1 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
2 (Data Constructor) | Idris.IdeMode |
errContext | Idris.AbsSyntax |
errEnv | Idris.Core.Typecheck |
ERROR | IRTS.Bytecode |
Error | Idris.Core.TT |
ErrorHandler | Idris.AbsSyntaxTree, Idris.AbsSyntax |
ErrorReflection | Idris.AbsSyntaxTree, Idris.AbsSyntax |
ErrorReportPart | Idris.Core.TT |
ErrorReverse | Idris.AbsSyntaxTree, Idris.AbsSyntax |
ErrPPrint | Idris.IdeMode |
errReverse | Idris.ErrReverse |
errSpan | Idris.AbsSyntaxTree, Idris.AbsSyntax |
ErrString | Idris.IdeMode |
erun | Idris.Core.Elaborate |
ES | Idris.Core.Elaborate |
EState | |
1 (Type/Class) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
ETyDecl | Idris.ElabTerm |
ETypes | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Eval | Idris.AbsSyntaxTree, Idris.AbsSyntax |
EvalApply | IRTS.Defunctionalise |
EvalCase | IRTS.Defunctionalise |
evalD | IRTS.Inliner |
EvalExpr | Idris.AbsSyntaxTree, Idris.AbsSyntax |
EvalIn | Idris.Core.ProofState, Idris.Core.Elaborate |
eval_in | Idris.Core.Elaborate |
Exact | |
1 (Data Constructor) | Idris.Core.ProofState, Idris.Core.Elaborate |
2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
exact | Idris.Core.Elaborate |
Example | Idris.Docstrings |
execElab | Idris.Core.Elaborate |
execScript | Idris.REPL |
Executable | IRTS.CodegenCommon |
Execute | Idris.AbsSyntaxTree, Idris.AbsSyntax |
execute | Idris.Core.Execute |
ExecVal | Idris.AbsSyntaxTree, Idris.AbsSyntax |
existsCon | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Exp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
expandDo | Idris.DSL |
ExpandLet | Idris.Core.ProofState, Idris.Core.Elaborate |
expandLet | Idris.Core.Elaborate |
expandNS | Idris.AbsSyntaxTree, Idris.AbsSyntax |
expandParams | Idris.AbsSyntax |
expandParamsD | Idris.AbsSyntax |
ExpectedType | Idris.Core.TT |
expl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
explicit | Idris.Core.Elaborate |
ExplicitD | Idris.PartialEval |
explicitNames | Idris.Core.TT |
ExplicitS | Idris.PartialEval |
expl_param | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Export | |
1 (Data Constructor) | IRTS.Lang, IRTS.Defunctionalise |
2 (Type/Class) | IRTS.Lang, IRTS.Defunctionalise |
ExportData | IRTS.Lang, IRTS.Defunctionalise |
exportDecls | IRTS.CodegenCommon |
ExportFun | IRTS.Lang, IRTS.Defunctionalise |
ExportIFace | IRTS.Lang, IRTS.Defunctionalise |
Expr | Idris.AbsSyntaxTree, Idris.AbsSyntax |
expr | Idris.ParseExpr, Idris.Parser |
expr' | Idris.ParseExpr, Idris.Parser |
ExprArg | Idris.Help |
ExprTArg | Idris.ParseExpr, Idris.Parser |
Extension | Idris.AbsSyntaxTree, Idris.AbsSyntax |
extension | Idris.ParseExpr, Idris.Parser |
extensions | Idris.ParseExpr, Idris.Parser |
externalExpr | Idris.ParseExpr, Idris.Parser |
ExternalIO | Idris.Core.Evaluate |
extractUnquotes | Idris.ElabQuasiquote |
extraHelp | Idris.Help |
e_guarded | Idris.ElabTerm |
e_inarg | Idris.ElabTerm |
e_intype | Idris.ElabTerm |
e_isfn | Idris.ElabTerm |
e_nomatching | Idris.ElabTerm |
e_qq | Idris.ElabTerm |