EAbandon | Idris.AbsSyntaxTree, Idris.AbsSyntax |
EAll | Idris.AbsSyntaxTree, Idris.AbsSyntax |
ECheck | Idris.AbsSyntaxTree, Idris.AbsSyntax |
EDefns | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Edit | Idris.REPL.Commands |
EDocStr | Idris.AbsSyntaxTree, Idris.AbsSyntax |
EEval | Idris.AbsSyntaxTree, Idris.AbsSyntax |
eEVAL | IRTS.Defunctionalise |
EImpossible | Idris.Elab.Term |
EInfo | Idris.AbsSyntaxTree, Idris.AbsSyntax |
eInfoNames | Idris.AbsSyntaxTree, Idris.AbsSyntax |
EitherErr | Idris.AbsSyntax |
Elab | Idris.Core.Elaborate |
elab | Idris.Elab.Term |
Elab' | Idris.Core.Elaborate |
elabCaseBlock | Idris.Elab.Utils |
elabCats | Idris.AbsSyntaxTree, Idris.AbsSyntax |
elabClause | Idris.Elab.Clause |
elabClauses | Idris.Elab.Clause |
ElabCtxt | |
1 (Type/Class) | Idris.Elab.Term |
2 (Data Constructor) | Idris.Elab.Term |
ElabD | Idris.AbsSyntaxTree, Idris.AbsSyntax |
elabData | Idris.Elab.Data |
elabDecl | Idris.ElabDecls |
elabDecl' | Idris.ElabDecls |
elabDecls | Idris.ElabDecls |
elabDocTerms | Idris.Elab.Value |
elabExec | Idris.Elab.Value |
elabExtern | Idris.Elab.Type |
elabFC | Idris.AbsSyntaxTree, Idris.AbsSyntax |
elabImplementation | Idris.Elab.Implementation |
ElabInfo | Idris.AbsSyntaxTree, Idris.AbsSyntax |
elabInterface | Idris.Elab.Interface |
elabMain | Idris.ElabDecls |
ElabMode | Idris.Elab.Term |
elaborate | Idris.Core.Elaborate |
Elaborating | Idris.Core.TT |
ElaboratingArg | Idris.Core.TT |
elaboratingArgErr | Idris.Elab.Term |
elaborating_app | Idris.Core.Elaborate |
elabPE | Idris.Elab.Clause |
elabPostulate | Idris.Elab.Type |
elabPrims | Idris.ElabDecls |
elabProvider | Idris.Elab.Provider |
elabRecord | Idris.Elab.Record |
ElabReflection | Idris.AbsSyntaxTree, Idris.AbsSyntax |
elabREPL | Idris.Elab.Value |
ElabResult | |
1 (Type/Class) | Idris.Elab.Term |
2 (Data Constructor) | Idris.Elab.Term |
elabRewrite | Idris.Elab.Rewrite |
elabRewriteLemma | Idris.Elab.Rewrite |
elabRunElab | Idris.Elab.RunElab |
ElabScriptDebug | Idris.Core.TT |
ElabScriptStaging | Idris.Core.TT |
ElabScriptStuck | Idris.Core.TT |
ElabShellCmd | Idris.AbsSyntaxTree, Idris.AbsSyntax |
ElabState | Idris.Core.Elaborate |
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.Elab.Term |
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 |
envBinders | Idris.Core.TT |
envlen | Idris.Core.TT |
EnvTT | Idris.Core.TT |
envTupleType | Idris.Reflection |
envZero | Idris.Core.TT |
eol | Idris.Parser.Helpers, Idris.Parser |
EProofState | Idris.AbsSyntaxTree, Idris.AbsSyntax |
EProofTerm | Idris.AbsSyntaxTree, Idris.AbsSyntax |
eqCon | Idris.AbsSyntaxTree, Idris.AbsSyntax |
eqDecl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
eqDoc | Idris.AbsSyntaxTree, Idris.AbsSyntax |
EQED | Idris.AbsSyntaxTree, Idris.AbsSyntax |
eqOpts | Idris.AbsSyntaxTree, Idris.AbsSyntax |
eqParamDoc | Idris.AbsSyntaxTree, Idris.AbsSyntax |
eqProp | Idris.Parser.Helpers, 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 |
erasure | Idris.Reflection |
ErasureInfo | Idris.Core.CaseTree |
ERHS | Idris.Elab.Term |
Err | Idris.Core.TT |
Err' | Idris.Core.TT |
errAt | Idris.Core.Elaborate |
ErrContext | |
1 (Data Constructor) | Idris.IdeMode |
2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
errContext | Idris.AbsSyntax |
errEnv | Idris.Core.Typecheck |
ERROR | IRTS.Bytecode |
Error | Idris.Core.TT |
ErrorHandler | Idris.AbsSyntaxTree, Idris.AbsSyntax |
ErrorReduce | 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 |
erunAux | Idris.Core.Elaborate |
ES | Idris.Core.Elaborate |
ESearch | Idris.AbsSyntaxTree, Idris.AbsSyntax |
EState | |
1 (Type/Class) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
ETransLHS | Idris.Elab.Term |
ETyDecl | Idris.Elab.Term |
ETypes | Idris.AbsSyntaxTree, Idris.AbsSyntax |
EUndo | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Eval | Idris.REPL.Commands |
EvalApply | IRTS.Defunctionalise |
EvalCase | IRTS.Defunctionalise |
evalD | IRTS.Inliner |
EvalExpr | Idris.AbsSyntaxTree, Idris.AbsSyntax |
EvalIn | Idris.Core.ProofState, Idris.Core.Elaborate |
EvalTypes | Idris.AbsSyntaxTree, Idris.AbsSyntax |
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 |
ExactlyOne | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Example | Idris.Docstrings |
execElab | Idris.Core.Elaborate |
execout | Idris.Package.Common |
Executable | IRTS.CodegenCommon |
Execute | Idris.REPL.Commands |
execute | Idris.Core.Execute |
ExecVal | Idris.REPL.Commands |
Exp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
expandImplementationScope | Idris.AbsSyntax |
ExpandLet | Idris.Core.ProofState, Idris.Core.Elaborate |
expandLet | Idris.Core.Elaborate |
expandNS | Idris.AbsSyntaxTree, Idris.AbsSyntax |
expandParams | Idris.AbsSyntax |
expandParamsD | Idris.AbsSyntax |
expandSugar | Idris.DSL |
expArg | Idris.AbsSyntax |
ExpectedType | Idris.Core.TT |
expl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
explicit | Idris.Core.Elaborate |
ExplicitD | Idris.PartialEval |
explicitNames | Idris.Core.TT |
explicitPi | Idris.Parser.Expr, Idris.Parser |
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.Parser.Expr, Idris.Parser |
expr' | Idris.Parser.Expr, Idris.Parser |
ExprArg | Idris.Help |
ExprTArg | Idris.Parser.Expr, Idris.Parser |
Extension | Idris.AbsSyntaxTree, Idris.AbsSyntax |
extension | Idris.Parser.Expr, Idris.Parser |
extensions | Idris.Parser.Expr, Idris.Parser |
externalDecl | Idris.Parser |
externalExpr | Idris.Parser.Expr, Idris.Parser |
ExternalIO | Idris.Core.Evaluate |
extractUnquotes | Idris.Elab.Quasiquote |
extraHelp | Idris.Help |
e_guarded | Idris.Elab.Term |
e_inarg | Idris.Elab.Term |
e_intype | Idris.Elab.Term |
e_isfn | Idris.Elab.Term |
e_nomatching | Idris.Elab.Term |
e_qq | Idris.Elab.Term |