Index - E
| eAbstractMode | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eActiveBackendName | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eActiveProblems | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eAllowedReductions | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eAnonymousModules | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eAppDef | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eAssignMetas | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eatNextChar | Mikan.Syntax.Parser.LookAhead |
| eCall | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eCallByNeed | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eChasePrefix | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eCheckingWhere | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eCheckpoints | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eClause | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eCompareBlocked | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eContext | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eCoverageCheck | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eCurrentCheckpoint | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eCurrentlyElaborating | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eCurrentModule | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eCurrentOpaqueId | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eCurrentPath | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| Edge | |
| 1 (Type/Class) | Mikan.Utils.Graph.AdjacencyMap.Unidirectional |
| 2 (Data Constructor) | Mikan.Utils.Graph.AdjacencyMap.Unidirectional |
| 3 (Type/Class) | Mikan.TypeChecking.Positivity.Occurrence, Mikan.TypeChecking.Positivity.OccurrenceAnalysis |
| 4 (Data Constructor) | Mikan.TypeChecking.Positivity.Occurrence, Mikan.TypeChecking.Positivity.OccurrenceAnalysis |
| edges | Mikan.Utils.Graph.AdjacencyMap.Unidirectional |
| edgesFrom | Mikan.Utils.Graph.AdjacencyMap.Unidirectional |
| edgesTo | Mikan.Utils.Graph.AdjacencyMap.Unidirectional |
| eDisplayFormsEnabled | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| editDistance | Mikan.Utils.List |
| eExpandLast | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eExpandLastBool | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| efExists | Mikan.Interaction.Library.Base |
| eFoldLetBindings | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| efPath | Mikan.Interaction.Library.Base |
| eGeneralizedVars | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eGeneralizeMetas | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eHardErrors | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eHighlightingLevel | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eHighlightingMethod | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eHighlightingRange | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eImportStack | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eInjectivityDepth | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eInsideDotPattern | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eInstanceDepth | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eIsDebugPrinting | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| Either3 | Mikan.Utils.Three |
| eitherDecode | Mikan.Interaction.JSON |
| eitherDecode' | Mikan.Interaction.JSON |
| eitherDecodeFileStrict | Mikan.Interaction.JSON |
| eitherDecodeFileStrict' | Mikan.Interaction.JSON |
| eitherDecodeStrict | Mikan.Interaction.JSON |
| eitherDecodeStrict' | Mikan.Interaction.JSON |
| eitherDecodeStrictText | Mikan.Interaction.JSON |
| El | Mikan.Syntax.Internal.Term |
| el | Mikan.TypeChecking.Primitive.Base, Mikan.TypeChecking.Primitive |
| el' | Mikan.TypeChecking.Primitive.Base, Mikan.TypeChecking.Primitive |
| el's | Mikan.TypeChecking.Primitive.Base, Mikan.TypeChecking.Primitive |
| ElaborateGive | Mikan.Interaction.InteractionTop |
| elaborate_give | Mikan.Interaction.BasicOps |
| elemAt | |
| 1 (Function) | Mikan.Utils.Set |
| 2 (Function) | Mikan.Utils.Set1 |
| 3 (Function) | Mikan.Utils.Map1 |
| elemConForms | Mikan.TypeChecking.With |
| Element | Mikan.Utils.Zipper |
| element | Mikan.Utils.Lens, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| elementOf | Mikan.Utils.Lens, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| elementsOf | Mikan.Utils.Lens, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| elemKindsOfNames | Mikan.Syntax.Scope.Base |
| elems | |
| 1 (Function) | Mikan.Utils.Set |
| 2 (Function) | Mikan.Utils.Map1 |
| 3 (Function) | Mikan.Utils.Set1 |
| 4 (Function) | Mikan.Utils.BoolSet |
| 5 (Function) | Mikan.Utils.SmallSet |
| 6 (Function) | Mikan.Utils.BiMap |
| eLetBindings | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eligibleForProjectionLike | Mikan.TypeChecking.ProjectionLike |
| Elim | |
| 1 (Type/Class) | Mikan.Syntax.Internal.Term |
| 2 (Type/Class) | Mikan.Syntax.Reflected |
| Elim' | |
| 1 (Type/Class) | Mikan.Syntax.Internal.Elim, Mikan.Syntax.Internal.Term |
| 2 (Type/Class) | Mikan.Syntax.Reflected |
| ElimCmp | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| Eliminated | Mikan.TypeChecking.Primitive.Cubical.Base, Mikan.TypeChecking.Primitive.Cubical, Mikan.TypeChecking.Primitive |
| eliminateDeadCode | Mikan.TypeChecking.DeadCode |
| eliminateType | Mikan.TypeChecking.Records |
| eliminateType' | Mikan.TypeChecking.Records |
| elimNotCoinductive | Mikan.Termination.Monad |
| Elims | |
| 1 (Type/Class) | Mikan.Syntax.Internal.Term |
| 2 (Type/Class) | Mikan.Syntax.Reflected |
| ElimType | Mikan.TypeChecking.Records |
| elimView | Mikan.TypeChecking.ProjectionLike |
| elimViewAction | Mikan.TypeChecking.CheckInternal |
| elInf | Mikan.TypeChecking.Primitive.Base, Mikan.TypeChecking.Primitive |
| Ellipsis | Mikan.Syntax.Concrete |
| EllipsisP | Mikan.Syntax.Concrete |
| ellipsisRange | Mikan.Syntax.Common |
| ellipsisWithArgs | Mikan.Syntax.Common |
| els | Mikan.TypeChecking.Primitive.Base, Mikan.TypeChecking.Primitive |
| elSSet | Mikan.TypeChecking.Primitive.Base, Mikan.TypeChecking.Primitive |
| emacsLispFiles | Mikan.Setup.DataFiles |
| emacsModeArg | Mikan.Interaction.Options.Arguments |
| EmacsModeCommand | Mikan.Interaction.Options |
| EmacsModeCompile | Mikan.Interaction.Options |
| emacsModeDir | Mikan.Setup.DataFiles |
| EmacsModeLocate | Mikan.Interaction.Options |
| EmacsModeSetup | Mikan.Interaction.Options |
| emacsModeValues | Mikan.Interaction.Options.Arguments |
| eMakeCase | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| embedWriter | Mikan.Utils.Monad |
| EmbPrj | Mikan.TypeChecking.Serialise.Base |
| Empty | Mikan.Utils.Empty |
| empty | |
| 1 (Function) | Mikan.Utils.Set |
| 2 (Function) | Mikan.Utils.BoolSet |
| 3 (Function) | Mikan.Utils.VarSet |
| 4 (Function) | Mikan.Utils.Null, Mikan.Utils.Trie, Mikan.Utils.Range, Mikan.Interaction.Highlighting.Range |
| 5 (Function) | Mikan.Utils.SmallSet |
| 6 (Function) | Mikan.Utils.HashTable |
| 7 (Function) | Mikan.Utils.Graph.AdjacencyMap.Unidirectional |
| EmptyAbstract | Mikan.Syntax.Concrete.Definitions.Errors, Mikan.Syntax.Concrete.Definitions |
| EmptyAbstract_ | Mikan.Interaction.Options.Warnings |
| emptyCompKit | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| EmptyConstructor | Mikan.Syntax.Concrete.Definitions.Errors, Mikan.Syntax.Concrete.Definitions |
| EmptyConstructor_ | Mikan.Interaction.Options.Warnings |
| emptyDict | Mikan.TypeChecking.Serialise.Base |
| EmptyDT | Mikan.TypeChecking.DiscrimTree.Types |
| EmptyField | Mikan.Syntax.Concrete.Definitions.Errors, Mikan.Syntax.Concrete.Definitions |
| EmptyField_ | Mikan.Interaction.Options.Warnings |
| emptyFunction | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| emptyFunctionData | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| EmptyGeneralize | Mikan.Syntax.Concrete.Definitions.Errors, Mikan.Syntax.Concrete.Definitions |
| EmptyGeneralize_ | Mikan.Interaction.Options.Warnings |
| emptyIdiomBrkt | Mikan.Syntax.Concrete.Glyph, Mikan.Syntax.Concrete.Pretty |
| EmptyInstance | Mikan.Syntax.Concrete.Definitions.Errors, Mikan.Syntax.Concrete.Definitions |
| EmptyInstance_ | Mikan.Interaction.Options.Warnings |
| emptyLayout | Mikan.Syntax.Parser.Layout |
| emptyLibFile | Mikan.Interaction.Library.Base |
| EmptyMacro | Mikan.Syntax.Concrete.Definitions.Errors, Mikan.Syntax.Concrete.Definitions |
| EmptyMacro_ | Mikan.Interaction.Options.Warnings |
| emptyMetaInfo | Mikan.Syntax.Info |
| emptyMimerStats | Mikan.Mimer.Types |
| EmptyMutual | Mikan.Syntax.Concrete.Definitions.Errors, Mikan.Syntax.Concrete.Definitions |
| EmptyMutual_ | Mikan.Interaction.Options.Warnings |
| emptyNameSpace | Mikan.Syntax.Scope.Base |
| EmptyPolarityPragma | Mikan.Syntax.Concrete.Definitions.Errors, Mikan.Syntax.Concrete.Definitions |
| EmptyPolarityPragma_ | Mikan.Interaction.Options.Warnings |
| EmptyPostulate | Mikan.Syntax.Concrete.Definitions.Errors, Mikan.Syntax.Concrete.Definitions |
| EmptyPostulate_ | Mikan.Interaction.Options.Warnings |
| EmptyPrimitive | Mikan.Syntax.Concrete.Definitions.Errors, Mikan.Syntax.Concrete.Definitions |
| EmptyPrimitive_ | Mikan.Interaction.Options.Warnings |
| EmptyPrivate | Mikan.Syntax.Concrete.Definitions.Errors, Mikan.Syntax.Concrete.Definitions |
| EmptyPrivate_ | Mikan.Interaction.Options.Warnings |
| emptyRecordDirectives | Mikan.Syntax.Common |
| EmptyS | Mikan.Syntax.Internal.Term, Mikan.TypeChecking.Substitute |
| emptyScope | Mikan.Syntax.Scope.Base |
| emptyScopeInfo | Mikan.Syntax.Scope.Base |
| emptySignature | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| EmptyTel | Mikan.Syntax.Internal.Telescope |
| EmptyTt | Mikan.Syntax.Internal.Telescope |
| EmptyWhere | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| EmptyWhere_ | Mikan.Interaction.Options.Warnings |
| empty_layout | Mikan.Syntax.Parser.Lexer |
| eMutualBlock | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| enableCaching | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| enableDisplayForms | Mikan.TypeChecking.Monad.Options, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| encode | |
| 1 (Function) | Mikan.Interaction.JSON |
| 2 (Function) | Mikan.TypeChecking.Serialise |
| Encoded | Mikan.TypeChecking.Serialise |
| EncodedDiagnostic | |
| 1 (Type/Class) | Mikan.TypeChecking.Monad.Diagnostic, Mikan.TypeChecking.Monad, Mikan.TypeChecking.Errors, Mikan.Compiler.Backend |
| 2 (Data Constructor) | Mikan.TypeChecking.Monad.Diagnostic, Mikan.TypeChecking.Monad, Mikan.TypeChecking.Errors, Mikan.Compiler.Backend |
| encodeFile | |
| 1 (Function) | Mikan.Interaction.JSON |
| 2 (Function) | Mikan.TypeChecking.Serialise |
| EncodeTCM | Mikan.Interaction.JSON |
| encodeTCM | Mikan.Interaction.JSON |
| Encoding | Mikan.Interaction.JSON |
| End | Mikan.Syntax.Common |
| end | Mikan.Syntax.Parser.LexActions |
| Endo | |
| 1 (Type/Class) | Mikan.Utils.StrictEndo |
| 2 (Data Constructor) | Mikan.Utils.StrictEndo |
| 3 (Type/Class) | Mikan.Utils.StrictFlipEndo |
| 4 (Data Constructor) | Mikan.Utils.StrictFlipEndo |
| EndoSubst | Mikan.TypeChecking.Substitute.Class, Mikan.TypeChecking.Substitute |
| endsInLevelTester | Mikan.Mimer.Monad |
| endWith | Mikan.Syntax.Parser.LexActions |
| end_ | Mikan.Syntax.Parser.LexActions |
| ensure | Mikan.Utils.Serialize |
| ensureCon | Mikan.TypeChecking.Unquote |
| ensureDef | Mikan.TypeChecking.Unquote |
| ensureEmptyType | Mikan.TypeChecking.Empty |
| ensureNPatterns | Mikan.TypeChecking.CompiledClause.Compile |
| ensureUnqual | Mikan.Syntax.Parser.Helpers |
| enterClosure | Mikan.TypeChecking.Monad.Closure, Mikan.TypeChecking.Monad, Mikan.TypeChecking.Reduce.Monad, Mikan.Compiler.Backend |
| EnterSection | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| enum | Mikan.Utils.Lens, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envAbstractMode | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envActiveBackendName | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envActiveProblems | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envAllowedReductions | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envAnonymousModules | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envAppDef | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envAssignMetas | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envCall | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envCallByNeed | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envChasePrefix | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envCheckingWhere | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envCheckpoints | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envClause | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envColdEnv | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envCompareBlocked | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envContext | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envCoverageCheck | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envCurrentCheckpoint | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envCurrentlyElaborating | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envCurrentModule | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envCurrentOpaqueId | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envCurrentPath | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envDisplayFormsEnabled | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envExpandLast | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envFlags | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envFoldLetBindings | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envGeneralizedVars | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envGeneralizeMetas | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envHardErrors | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envHighlightingLevel | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envHighlightingMethod | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envHighlightingRange | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envImportStack | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envInjectivityDepth | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envInsideDotPattern | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envInstanceDepth | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| environmentColor | Mikan.Utils.IO.Terminal |
| envIsDebugPrinting | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envLetBindings | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envMakeCase | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envMutualBlock | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envPrintDomainFreePi | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envPrintingPatternLambdas | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envPrintMetasBare | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envPureConversion | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envRange | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envReconstructed | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envReduceDefs | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envSimplification | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envSolvingConstraints | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envSplitOnStrict | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envTCContext | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envTerminationCheck | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envUnquoteFlags | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| envUnquoteProblem | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| EnvVars | Mikan.Utils.Environment |
| envWorkingOnTypes | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eof | Mikan.Syntax.Parser.LexActions |
| ePrintDomainFreePi | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| ePrintingPatternLambdas | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| ePrintMetasBare | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| ePureConversion | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eqConstructorForm | Mikan.TypeChecking.Rules.LHS.Unify.Types |
| eqCount | Mikan.TypeChecking.Rules.LHS.Unify.Types |
| eqLHS | Mikan.TypeChecking.Rules.LHS.Unify.Types |
| eqRHS | Mikan.TypeChecking.Rules.LHS.Unify.Types |
| eqTel | Mikan.TypeChecking.Rules.LHS.Unify.Types |
| eqtLhs | Mikan.TypeChecking.Monad.Builtin, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eqtName | Mikan.TypeChecking.Monad.Builtin, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eqtParams | Mikan.TypeChecking.Monad.Builtin, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eqtRange | Mikan.TypeChecking.Monad.Builtin, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eqtRhs | Mikan.TypeChecking.Monad.Builtin, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eqtSort | Mikan.TypeChecking.Monad.Builtin, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eqtType | Mikan.TypeChecking.Monad.Builtin, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| Equal | |
| 1 (Data Constructor) | Mikan.Syntax.Concrete |
| 2 (Data Constructor) | Mikan.TypeChecking.Rules.LHS.Unify.Types |
| equalAtom | Mikan.TypeChecking.Conversion |
| Equality | Mikan.TypeChecking.Rules.LHS.Unify.Types |
| EqualityType | Mikan.TypeChecking.Monad.Builtin, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| EqualityTypeData | |
| 1 (Type/Class) | Mikan.TypeChecking.Monad.Builtin, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| 2 (Data Constructor) | Mikan.TypeChecking.Monad.Builtin, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| EqualityUnview | Mikan.TypeChecking.Monad.Builtin, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| equalityUnview | Mikan.TypeChecking.Monad.Builtin, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| EqualityView | Mikan.TypeChecking.Monad.Builtin, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| equalityView | Mikan.TypeChecking.Monad.Builtin, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| EqualityViewType | Mikan.TypeChecking.Monad.Builtin, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| equalLevel | Mikan.TypeChecking.Conversion |
| EqualP | |
| 1 (Data Constructor) | Mikan.Syntax.Concrete |
| 2 (Data Constructor) | Mikan.Syntax.Abstract |
| equals | |
| 1 (Function) | Mikan.Syntax.Common.Pretty |
| 2 (Function) | Mikan.TypeChecking.Pretty |
| equalSort | Mikan.TypeChecking.Conversion |
| EqualSy | Mikan.TypeChecking.Abstract |
| equalSy | Mikan.TypeChecking.Abstract |
| equalTerm | Mikan.TypeChecking.Conversion |
| equalTermOnFace | Mikan.TypeChecking.Conversion |
| equalTermToBoundary | Mikan.TypeChecking.Conversion |
| equalType | Mikan.TypeChecking.Conversion |
| eqUnLevel | Mikan.TypeChecking.Rules.LHS.Unify.Types |
| eRange | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eraseSBool | Mikan.Utils.TypeLits |
| eReconstructed | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eReduceDefs | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eReduceDefsPair | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| errClosure | Mikan.TypeChecking.Errors.Deferred |
| errInput | Mikan.Syntax.Parser.Monad, Mikan.Syntax.Parser |
| errIOError | Mikan.Syntax.Parser.Monad, Mikan.Syntax.Parser |
| errLoc | Mikan.TypeChecking.Errors.Deferred |
| errMsg | Mikan.Syntax.Parser.Monad, Mikan.Syntax.Parser |
| Error | |
| 1 (Data Constructor) | Mikan.Syntax.Common.Aspect, Mikan.Interaction.Highlighting.Precise |
| 2 (Data Constructor) | Mikan.Interaction.Base |
| errorConflictingAttribute | Mikan.Syntax.Parser.Helpers |
| errorConflictingAttributes | Mikan.Syntax.Parser.Helpers |
| errorHighlighting | Mikan.Interaction.Highlighting.Generate |
| ErrorName | Mikan.Interaction.Options.Errors |
| errorNameString | Mikan.Interaction.Options.Errors |
| ErrorPart | Mikan.TypeChecking.Unquote |
| errorType | Mikan.TypeChecking.Primitive.Cubical, Mikan.TypeChecking.Primitive |
| ErrorWarning | Mikan.Syntax.Common.Aspect, Mikan.Interaction.Highlighting.Precise |
| ErrorWarnings | Mikan.TypeChecking.Warnings |
| errorWarnings | Mikan.Interaction.Options.Warnings |
| errPath | Mikan.Syntax.Parser.Monad, Mikan.Syntax.Parser |
| errPos | Mikan.Syntax.Parser.Monad, Mikan.Syntax.Parser |
| errPrevToken | Mikan.Syntax.Parser.Monad, Mikan.Syntax.Parser |
| errRange | Mikan.Syntax.Parser.Monad, Mikan.Syntax.Parser |
| errState | Mikan.TypeChecking.Errors.Deferred |
| errValidExts | Mikan.Syntax.Parser.Monad, Mikan.Syntax.Parser |
| escape | Mikan.Interaction.Highlighting.Vim |
| escapeContext | Mikan.TypeChecking.Monad.Context, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| EscapingVariable | Mikan.TypeChecking.Unquote.Errors |
| eSimplification | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eSolvingConstraints | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eSplitOnStrict | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| Eta | Mikan.Syntax.Concrete |
| etaBranch | Mikan.TypeChecking.CompiledClause |
| etaCase | Mikan.TypeChecking.CompiledClause |
| etaCon | Mikan.TypeChecking.EtaContract |
| etaContract | Mikan.TypeChecking.EtaContract |
| etaContractRecord | Mikan.TypeChecking.Records |
| etaEnabled | Mikan.TypeChecking.Monad.Options, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| EtaEquality | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| EtaExpand | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| etaExpandAtRecordType | Mikan.TypeChecking.Records |
| etaExpandBlocked | Mikan.TypeChecking.MetaVars |
| etaExpandBoundVar | Mikan.TypeChecking.Records |
| etaExpandClause | Mikan.TypeChecking.Functions |
| EtaExpandEquation | Mikan.TypeChecking.Rules.LHS.Unify.Types |
| etaExpandListeners | Mikan.TypeChecking.Monad.MetaVars, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| etaExpandMeta | Mikan.TypeChecking.Monad.MetaVars, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| etaExpandMetaSafe | Mikan.TypeChecking.Monad.MetaVars, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| etaExpandMetaTCM | Mikan.TypeChecking.MetaVars |
| etaExpandProjectedVar | Mikan.TypeChecking.MetaVars |
| etaExpandRecord | Mikan.TypeChecking.Records |
| etaExpandRecord' | Mikan.TypeChecking.Records |
| etaExpandRecord'_ | Mikan.TypeChecking.Records |
| etaExpandRecord_ | Mikan.TypeChecking.Records |
| EtaExpandVar | Mikan.TypeChecking.Rules.LHS.Unify.Types |
| etaLam | Mikan.TypeChecking.EtaContract |
| etaOnce | Mikan.TypeChecking.EtaContract |
| EtaPragma | |
| 1 (Data Constructor) | Mikan.Syntax.Concrete |
| 2 (Data Constructor) | Mikan.Syntax.Abstract |
| eTerminationCheck | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eUnquoteFlags | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eUnquoteNormalise | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| eUnquoteProblem | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| evalInCurrent | Mikan.Interaction.BasicOps |
| evalInMeta | Mikan.Interaction.BasicOps |
| evalState | |
| 1 (Function) | Mikan.Utils.StrictState |
| 2 (Function) | Mikan.Utils.StrictState2 |
| evalStateT | Mikan.Utils.StrictState |
| evalTCM | Mikan.TypeChecking.Unquote |
| evalUpdater | Mikan.Utils.Update |
| evalWithScope | Mikan.TypeChecking.Monad.State, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| everyPrefix | Mikan.Utils.Trie |
| everythingInScope | Mikan.Syntax.Scope.Base |
| eWorkingOnTypes | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| exact | Mikan.Interaction.Base |
| exactConInduction | Mikan.Syntax.Scope.Base |
| exactConName | Mikan.Syntax.Scope.Base |
| exactSplitWarnings | Mikan.Interaction.Options.Warnings |
| ExceptKindsOfNames | Mikan.Syntax.Scope.Base |
| exceptKindsOfNames | Mikan.Syntax.Scope.Base |
| ExeArg | Mikan.TypeChecking.Unquote |
| ExecError | Mikan.TypeChecking.Unquote.Errors |
| execErrorNameString | Mikan.Interaction.Options.Errors |
| ExecError_ | |
| 1 (Data Constructor) | Mikan.Interaction.Options.Errors |
| 2 (Type/Class) | Mikan.Interaction.Options.Errors |
| execState | |
| 1 (Function) | Mikan.Utils.StrictState |
| 2 (Function) | Mikan.Utils.StrictState2 |
| execStateT | Mikan.Utils.StrictState |
| ExecutablesFile | |
| 1 (Type/Class) | Mikan.Interaction.Library.Base |
| 2 (Data Constructor) | Mikan.Interaction.Library.Base |
| execWriter | Mikan.Utils.StrictWriter |
| execWriterT | Mikan.Utils.StrictWriter |
| ExeMap | Mikan.Interaction.Library.Base |
| ExeName | Mikan.Interaction.Library.Base, Mikan.Interaction.Library |
| ExeNotExecutable | Mikan.TypeChecking.Unquote.Errors |
| ExeNotExecutable_ | Mikan.Interaction.Options.Errors |
| ExeNotFound | Mikan.TypeChecking.Unquote.Errors |
| ExeNotFound_ | Mikan.Interaction.Options.Errors |
| ExeNotTrusted | Mikan.TypeChecking.Unquote.Errors |
| ExeNotTrusted_ | Mikan.Interaction.Options.Errors |
| existsM | Mikan.Utils.Monad |
| exitAgdaWith | Mikan.Interaction.ExitCode |
| exitCodeToNat | Mikan.TypeChecking.Unquote |
| exitSuccess | Mikan.Interaction.ExitCode |
| expand | Mikan.Utils.ExpandCase |
| expandAt | Mikan.TypeChecking.Rules.LHS.Unify.Types |
| ExpandBoth | Mikan.TypeChecking.Rules.LHS.Problem |
| ExpandCase | Mikan.Utils.ExpandCase |
| expandCatchalls | Mikan.TypeChecking.CompiledClause.Compile |
| ExpandedEllipsis | |
| 1 (Type/Class) | Mikan.Syntax.Common |
| 2 (Data Constructor) | Mikan.Syntax.Common |
| ExpandedPun | Mikan.Syntax.Common |
| expandEnvironmentVariables | Mikan.Utils.Environment |
| expandEnvVarTelescope | Mikan.Utils.Environment |
| ExpandHidden | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| ExpandLast | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| expandLitPattern | Mikan.TypeChecking.Patterns.Abstract |
| expandModuleAssigns | Mikan.TypeChecking.Rules.Term |
| expandP | Mikan.Utils.Permutation |
| expandParameters | Mikan.TypeChecking.Rules.LHS.Unify.Types |
| ExpandPatternSynonyms | Mikan.TypeChecking.Patterns.Abstract |
| expandPatternSynonyms | Mikan.TypeChecking.Patterns.Abstract |
| expandPatternSynonyms' | Mikan.TypeChecking.Patterns.Abstract |
| expandProjectedVars | Mikan.TypeChecking.MetaVars |
| expandRecordType | Mikan.TypeChecking.Rules.LHS.Unify.Types |
| expandRecordVar | Mikan.TypeChecking.Records |
| expandRecordVarsRecursively | Mikan.TypeChecking.Records |
| expandTelescopeVar | Mikan.TypeChecking.Telescope |
| expandVar | Mikan.TypeChecking.Rules.LHS.Unify.Types |
| expandVarParameters | Mikan.TypeChecking.Rules.LHS.Unify.Types |
| expandVarRecordType | Mikan.TypeChecking.Rules.LHS.Unify.Types |
| ExpectedApplication | Mikan.Interaction.Errors |
| ExpectedBindingForParameter_ | Mikan.Interaction.Options.Errors |
| ExpectedIdentifier | Mikan.Interaction.Errors |
| ExpectedIntervalLiteral | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| ExpectedIntervalLiteral_ | Mikan.Interaction.Options.Errors |
| explainStep | Mikan.TypeChecking.Rules.LHS.Unify.LeftInverse |
| explainWhyInScope | Mikan.TypeChecking.Errors, Mikan.Interaction.EmacsTop |
| explicitToField | Mikan.Interaction.JSON |
| explicitToFieldOmit | Mikan.Interaction.JSON |
| exportedNamesInScope | Mikan.Syntax.Scope.Base |
| Expr | |
| 1 (Type/Class) | Mikan.Syntax.Concrete |
| 2 (Type/Class) | Mikan.Syntax.Abstract |
| exprAsNameAndPattern | Mikan.Syntax.Parser.Helpers |
| exprAsNameOrHiddenNames | Mikan.Syntax.Parser.Helpers |
| exprAsNamesAndPatterns | Mikan.Syntax.Parser.Helpers |
| exprFieldA | Mikan.Syntax.Concrete |
| ExprHole | Mikan.Syntax.Notation |
| ExprInfo | Mikan.Syntax.Info |
| ExprKind | Mikan.Syntax.Common |
| ExprLike | |
| 1 (Type/Class) | Mikan.Syntax.Concrete.Generic |
| 2 (Type/Class) | Mikan.Syntax.Abstract.Views |
| exprNoRange | Mikan.Syntax.Info |
| exprParser | |
| 1 (Function) | Mikan.Syntax.Parser.Parser |
| 2 (Function) | Mikan.Syntax.Parser |
| ExprRange | Mikan.Syntax.Info |
| exprToAssignment | Mikan.Syntax.Parser.Helpers |
| exprToAttribute | Mikan.Syntax.Concrete.Attribute |
| exprToLHS | Mikan.Syntax.Parser.Helpers |
| exprToName | Mikan.Syntax.Parser.Helpers |
| exprToPattern | Mikan.Syntax.Parser.Helpers |
| exprToPatternWithHoles | Mikan.Syntax.Concrete |
| ExprView | Mikan.Syntax.Concrete.Operators.Parser |
| exprView | Mikan.Syntax.Concrete.Operators.Parser |
| ExprWhere | |
| 1 (Type/Class) | Mikan.Syntax.Concrete |
| 2 (Data Constructor) | Mikan.Syntax.Concrete |
| exprWhereParser | |
| 1 (Function) | Mikan.Syntax.Parser.Parser |
| 2 (Function) | Mikan.Syntax.Parser |
| expS | Mikan.TypeChecking.Primitive.Cubical, Mikan.TypeChecking.Primitive |
| expTelescope | Mikan.TypeChecking.Primitive.Cubical, Mikan.TypeChecking.Primitive |
| extended | Mikan.Interaction.Options.BashCompletion |
| ExtendedLam | |
| 1 (Data Constructor) | Mikan.Syntax.Concrete |
| 2 (Data Constructor) | Mikan.Syntax.Abstract |
| ExtendedLambda | Mikan.Interaction.Response.Base, Mikan.Interaction.Response |
| extendedLambdaName | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| extendInferredBlock | Mikan.Syntax.Concrete.Definitions.Types |
| extendReduceEnv | Mikan.TypeChecking.Monad.Context, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| ExtendTel | Mikan.Syntax.Internal.Telescope |
| ExtendTt | Mikan.Syntax.Internal.Telescope |
| ExtLam | Mikan.Syntax.Reflected |
| extLam | Mikan.Syntax.Parser.Helpers |
| extLamAbsurd | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| ExtLamInfo | |
| 1 (Type/Class) | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| 2 (Data Constructor) | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| extLamModule | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| extLamSys | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| extlam_dropName | Mikan.Interaction.InteractionTop |
| extOrAbsLam | Mikan.Syntax.Parser.Helpers |
| extractParameters | Mikan.TypeChecking.ReconstructParameters |
| extractPattern | Mikan.Syntax.Abstract |