Index - C
| C | Mikan.Mimer.Options |
| cacheCurrentLog | Mikan.TypeChecking.Monad.Caching, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| CachedTypeCheckLog | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| cacheVar | Mikan.TypeChecking.Serialise.Base |
| cachingStarts | Mikan.TypeChecking.Monad.Caching, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| caElim | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| Call | |
| 1 (Type/Class) | Mikan.Termination.CallGraph |
| 2 (Type/Class) | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| callBackend | Mikan.Compiler.Backend |
| callBackendInteractHole | Mikan.Compiler.Backend |
| callBackendInteractTop | Mikan.Compiler.Backend |
| callByName | Mikan.TypeChecking.Monad.Env, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| CallComb | Mikan.Termination.CallMatrix |
| CallGraph | |
| 1 (Type/Class) | Mikan.Termination.CallGraph |
| 2 (Data Constructor) | Mikan.Termination.CallGraph |
| CallInfo | |
| 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 |
| callInfoCall | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| callInfos | Mikan.Termination.Monad |
| callInfoTarget | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| CallMatrix | |
| 1 (Type/Class) | Mikan.Termination.CallMatrix |
| 2 (Data Constructor) | Mikan.Termination.CallMatrix |
| CallMatrix' | Mikan.Termination.CallMatrix |
| CallMatrixAug | |
| 1 (Type/Class) | Mikan.Termination.CallMatrix |
| 2 (Data Constructor) | Mikan.Termination.CallMatrix |
| callMatrixSet | Mikan.Termination.CallGraph |
| CallPath | |
| 1 (Type/Class) | Mikan.Termination.Monad |
| 2 (Data Constructor) | Mikan.Termination.Monad |
| callPathStart | Mikan.Termination.Monad |
| callPathSteps | Mikan.Termination.Monad |
| CallSite | |
| 1 (Type/Class) | Mikan.Utils.CallStack |
| 2 (Data Constructor) | Mikan.Utils.CallStack |
| CallSiteFilter | Mikan.Utils.CallStack |
| CallStack | Mikan.Utils.CallStack |
| callStack | Mikan.Utils.CallStack |
| camelTo2 | Mikan.Interaction.JSON |
| Candidate | |
| 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 |
| CandidateKind | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| candidateKind | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| candidateOverlap | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| candidateTerm | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| candidateType | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| canDropRecursiveInstance | Mikan.TypeChecking.Monad.Constraints, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| canHaveSuffixTest | Mikan.Syntax.Scope.Monad |
| CannotApply | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| CannotApply_ | Mikan.Interaction.Options.Errors |
| CannotBeProjectionPattern | Mikan.Syntax.Concrete |
| CannotCreateMissingClause | Mikan.TypeChecking.Coverage.Errors |
| CannotCreateMissingClause_ | Mikan.Interaction.Options.Errors |
| CannotDeclareHiddenFunction | Mikan.TypeChecking.Unquote.Errors |
| CannotEliminateWithPattern | Mikan.TypeChecking.Coverage.Errors |
| CannotEliminateWithPattern_ | Mikan.Interaction.Options.Errors |
| CannotEliminateWithProjection | Mikan.TypeChecking.Coverage.Errors |
| CannotEliminateWithProjection_ | Mikan.Interaction.Options.Errors |
| CannotGeneralizeEtaExpandable | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| CannotGeneralizeEtaExpandable_ | Mikan.Interaction.Options.Errors |
| CannotGenerateTransportClause | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| CannotGenerateTransportClause_ | Mikan.Interaction.Options.Errors |
| CannotGive | Mikan.Interaction.Errors |
| CannotQuote | |
| 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 |
| CannotQuoteAmbiguous | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| CannotQuoteAmbiguous_ | Mikan.Interaction.Options.Errors |
| CannotQuoteExpression | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| CannotQuoteExpression_ | Mikan.Interaction.Options.Errors |
| CannotQuoteHidden | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| CannotQuoteHidden_ | Mikan.Interaction.Options.Errors |
| cannotQuoteNameString | Mikan.Interaction.Options.Errors |
| CannotQuoteNothing | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| CannotQuoteNothing_ | Mikan.Interaction.Options.Errors |
| CannotQuotePattern | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| CannotQuotePattern_ | Mikan.Interaction.Options.Errors |
| CannotQuoteTerm | |
| 1 (Type/Class) | Mikan.Interaction.Options.Errors, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| 2 (Data Constructor) | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| CannotQuoteTermHidden | Mikan.Interaction.Options.Errors, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| cannotQuoteTermNameString | Mikan.Interaction.Options.Errors |
| CannotQuoteTermNothing | Mikan.Interaction.Options.Errors, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| CannotQuoteTerm_ | Mikan.Interaction.Options.Errors |
| CannotQuote_ | |
| 1 (Type/Class) | Mikan.Interaction.Options.Errors |
| 2 (Data Constructor) | Mikan.Interaction.Options.Errors |
| CannotRefine | Mikan.Interaction.Errors |
| CannotResolveAmbiguousPatternSynonym | Mikan.Syntax.Scope.Errors |
| CannotResolveAmbiguousPatternSynonym_ | Mikan.Interaction.Options.Errors |
| CannotRewriteByNonEquation | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| CannotRewriteByNonEquation_ | Mikan.Interaction.Options.Errors |
| CannotTransp | Mikan.TypeChecking.Primitive.Cubical, Mikan.TypeChecking.Primitive |
| canonicalizeAbsolutePath | Mikan.Utils.FileName |
| canonicalName | Mikan.TypeChecking.Monad.Signature, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| canProject | Mikan.TypeChecking.Substitute |
| canSolveMetaOpaquely | Mikan.TypeChecking.Opacity |
| CantGeneralizeOverSorts | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| CantGeneralizeOverSorts_ | Mikan.Interaction.Options.Warnings |
| CantInvert | Mikan.TypeChecking.MetaVars |
| CantResolveOverloadedConstructorsTargetingSameDatatype | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| CantResolveOverloadedConstructorsTargetingSameDatatype_ | Mikan.Interaction.Options.Errors |
| cantSplitBlocker | Mikan.TypeChecking.Coverage.Errors |
| cantSplitConIdx | Mikan.TypeChecking.Coverage.Errors |
| cantSplitConName | Mikan.TypeChecking.Coverage.Errors |
| cantSplitFailures | Mikan.TypeChecking.Coverage.Errors |
| cantSplitGivenIdx | Mikan.TypeChecking.Coverage.Errors |
| cantSplitProjName | Mikan.TypeChecking.Coverage.Errors |
| cantSplitProjWhy | Mikan.TypeChecking.Coverage.Errors |
| cantSplitTel | Mikan.TypeChecking.Coverage.Errors |
| cantSplitType | Mikan.TypeChecking.Coverage.Errors |
| CantTransport | Mikan.TypeChecking.Rules.LHS.Unify.LeftInverse, Mikan.TypeChecking.Rules.LHS.Unify |
| CantTransport' | Mikan.TypeChecking.Rules.LHS.Unify.LeftInverse, Mikan.TypeChecking.Rules.LHS.Unify |
| capacity | Mikan.Utils.HashSet.Ordered |
| caRange | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| Carrier | Mikan.Utils.Zipper |
| cartesianProduct | |
| 1 (Function) | Mikan.Utils.Set |
| 2 (Function) | Mikan.Utils.Set1 |
| Case | |
| 1 (Type/Class) | Mikan.TypeChecking.CompiledClause |
| 2 (Data Constructor) | Mikan.TypeChecking.CompiledClause |
| CaseContext | Mikan.Interaction.MakeCase |
| CaseDT | Mikan.TypeChecking.DiscrimTree.Types |
| caseEitherM | Mikan.Utils.Either |
| caseList | Mikan.Utils.List |
| caseListM | Mikan.Utils.List |
| caseListT | Mikan.Utils.ListT |
| caseMaybe | |
| 1 (Function) | Mikan.Utils.Maybe.Strict |
| 2 (Function) | Mikan.Utils.Maybe |
| caseMaybeM | |
| 1 (Function) | Mikan.Utils.Maybe.Strict |
| 2 (Function) | Mikan.Utils.Maybe |
| CaseSplit | Mikan.Syntax.Common |
| CaseSplitError | Mikan.Interaction.Errors |
| cat | Mikan.Syntax.Common.Pretty |
| Catchall | Mikan.Syntax.Common |
| catchall | Mikan.TypeChecking.CompiledClause |
| catchallBranch | Mikan.TypeChecking.CompiledClause |
| CatchallClause | Mikan.Syntax.Common.Aspect, Mikan.Interaction.Highlighting.Precise |
| CatchallPragma | Mikan.Syntax.Concrete |
| catchallPragma | Mikan.Syntax.Concrete.Definitions.Monad |
| catchAndPrintImpossible | Mikan.TypeChecking.Monad.Debug, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| catchConstraint | Mikan.TypeChecking.Monad.Constraints, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| catchError_ | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| catchExceptT | Mikan.Utils.Monad |
| catchIlltypedPatternBlockedOnMeta | Mikan.TypeChecking.Rules.Term |
| CatchImpossible | Mikan.Utils.Impossible |
| catchImpossible | Mikan.Utils.Impossible |
| catchImpossibleJust | Mikan.Utils.Impossible |
| catchNull | Mikan.Utils.Null |
| catchPatternErr | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| catMaybe' | Mikan.Utils.List |
| catMaybes | |
| 1 (Function) | Mikan.Utils.Maybe |
| 2 (Function) | Mikan.Utils.Maybe.Strict |
| 3 (Function) | Mikan.Utils.List1 |
| catMaybesMP | Mikan.Utils.Monad |
| ccBody | Mikan.TypeChecking.CompiledClause |
| ccBoundVars | Mikan.TypeChecking.CompiledClause |
| ccClauseNumber | Mikan.TypeChecking.CompiledClause |
| ccClauseRecursive | Mikan.TypeChecking.CompiledClause |
| CCDone | |
| 1 (Type/Class) | Mikan.TypeChecking.CompiledClause |
| 2 (Data Constructor) | Mikan.TypeChecking.CompiledClause |
| ceName | Mikan.TypeChecking.Monad.Base.Types, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| censor | Mikan.Utils.StrictWriter |
| censoring | Mikan.Utils.Lens, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| ceType | Mikan.TypeChecking.Monad.Base.Types, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| Change | Mikan.Utils.Update |
| ChangeT | Mikan.Utils.Update |
| char | Mikan.Syntax.Common.Pretty |
| ChaseDisplayForms | Mikan.TypeChecking.Monad.Signature, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| chaseDisplayForms | Mikan.TypeChecking.Monad.Signature, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| chaseModule | Mikan.Interaction.Imports |
| checkAbsurdLambda | Mikan.TypeChecking.Rules.Term |
| checkAlias | Mikan.TypeChecking.Rules.Def |
| checkAndSetOptionsFromPragma | Mikan.TypeChecking.Monad.Options, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| checkApplication | Mikan.TypeChecking.Rules.Application |
| CheckArgs | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| CheckArguments | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| checkArguments | Mikan.TypeChecking.Rules.Application |
| checkArguments_ | Mikan.TypeChecking.Rules.Application |
| checkAxiom | Mikan.TypeChecking.Rules.Decl |
| checkAxiom' | Mikan.TypeChecking.Rules.Decl |
| CheckClause | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| checkClause | Mikan.TypeChecking.Rules.Def |
| checkClauseLHS | Mikan.TypeChecking.Rules.Def |
| checkClauseTelescopeBindings | Mikan.Syntax.Translation.ReflectedToAbstract |
| CheckConArgFitsIn | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| CheckConstraint | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| CheckConstructor | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| checkConstructor | Mikan.TypeChecking.Rules.Data |
| CheckDataDef | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| checkDataDef | Mikan.TypeChecking.Rules.Data |
| CheckDataSort | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| checkDataSort | Mikan.TypeChecking.Rules.Data |
| checkDecl | Mikan.TypeChecking.Rules.Decl, Mikan.TheTypeChecker |
| checkDeclCached | Mikan.TypeChecking.Rules.Decl, Mikan.TheTypeChecker |
| checkDecls | Mikan.TypeChecking.Rules.Decl, Mikan.TheTypeChecker |
| checkDisplayPragma | Mikan.TypeChecking.Rules.Display |
| checkDomain | Mikan.TypeChecking.Rules.Term |
| checkDontExpandLast | Mikan.TypeChecking.Rules.Term |
| CheckDotPattern | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| CheckedArg | |
| 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 |
| CheckedTarget | |
| 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 |
| checkEmptyTel | Mikan.TypeChecking.Empty |
| CheckExpr | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| checkExpr | Mikan.TypeChecking.Rules.Term, Mikan.TheTypeChecker |
| checkExpr' | Mikan.TypeChecking.Rules.Term |
| CheckExprCall | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| checkExtendedLambda | Mikan.TypeChecking.Rules.Term |
| checkForImportCycle | Mikan.TypeChecking.Monad.Imports, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| checkForUniqueAttribute | Mikan.Syntax.Parser.Helpers |
| CheckFunDef | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| checkFunDef | Mikan.TypeChecking.Rules.Def |
| checkFunDef' | Mikan.TypeChecking.Rules.Def |
| CheckFunDefCall | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| checkFunDefS | Mikan.TypeChecking.Rules.Def |
| checkGeneralize | Mikan.TypeChecking.Rules.Decl |
| checkGeneralizeTelescope | Mikan.TypeChecking.Rules.Term |
| CheckIApplyConfluence | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| checkIApplyConfluence | Mikan.TypeChecking.IApplyConfluence |
| checkIApplyConfluence_ | Mikan.TypeChecking.IApplyConfluence |
| CheckIndexSort | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| checkIndexSorts | Mikan.TypeChecking.Rules.Data |
| checkingWhere | Mikan.Syntax.Concrete.Definitions.Monad, Mikan.Syntax.Concrete.Definitions |
| checkInjectivity | Mikan.TypeChecking.Injectivity |
| checkInjectivity' | Mikan.TypeChecking.Injectivity |
| checkInjectivity_ | Mikan.TypeChecking.Rules.Decl |
| CheckInternal | Mikan.TypeChecking.CheckInternal |
| checkInternal | Mikan.TypeChecking.CheckInternal |
| checkInternal' | Mikan.TypeChecking.CheckInternal |
| CheckIsEmpty | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| checkKnownArgument | Mikan.TypeChecking.Rules.Term |
| checkKnownArguments | Mikan.TypeChecking.Rules.Term |
| checkLambda | Mikan.TypeChecking.Rules.Term |
| checkLambda' | Mikan.TypeChecking.Rules.Term |
| checkLazyMatch | Mikan.TypeChecking.CompiledClause |
| checkLeftHandSide | Mikan.TypeChecking.Rules.LHS |
| CheckLetBinding | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| checkLetBinding | Mikan.TypeChecking.Rules.Term |
| checkLetBinding' | Mikan.TypeChecking.Rules.Term |
| checkLetBindings | Mikan.TypeChecking.Rules.Term |
| checkLetBindings' | Mikan.TypeChecking.Rules.Term |
| checkLevel | Mikan.TypeChecking.Rules.Term |
| CheckLHS | |
| 1 (Data Constructor) | Mikan.Benchmarking, Mikan.TypeChecking.Monad.Benchmark |
| 2 (Data Constructor) | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| checkLibraryFileNotTooFarDown | Mikan.TypeChecking.Monad.Options, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| checkLinearity | Mikan.TypeChecking.MetaVars |
| checkLiteral | Mikan.TypeChecking.Rules.Term |
| CheckLock | Mikan.Interaction.Base |
| checkLoneSigs | Mikan.Syntax.Concrete.Definitions.Monad |
| checkMacroType | Mikan.TypeChecking.Rules.Def |
| checkMeta | Mikan.TypeChecking.Rules.Term |
| CheckMetaInst | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| checkMetaInst | Mikan.TypeChecking.MetaVars |
| CheckMetaSolution | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| checkModuleArity | Mikan.TypeChecking.Rules.Decl |
| checkModuleName | Mikan.Interaction.FindFile |
| CheckModuleParameters | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| checkMutual | Mikan.TypeChecking.Rules.Decl |
| checkNamedArg | Mikan.TypeChecking.Rules.Term |
| checkNoFixityInRenamingModule | Mikan.Syntax.Scope.Monad |
| CheckNonLocalWhere | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| checkNoShadowing | Mikan.Syntax.Scope.Monad |
| checkOpts | Mikan.Interaction.Options |
| checkOrInferMeta | Mikan.TypeChecking.Rules.Term |
| checkOverapplication | Mikan.TypeChecking.Injectivity |
| CheckOverlap | Mikan.Benchmarking, Mikan.TypeChecking.Monad.Benchmark |
| checkPath | Mikan.TypeChecking.Rules.Term |
| CheckPattern | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| checkPatternLinearity | Mikan.Syntax.Abstract.Pattern |
| CheckPatternLinearityType | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| CheckPatternLinearityValue | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| checkPiDomain | Mikan.TypeChecking.Rules.Term |
| checkPiTelescope | Mikan.TypeChecking.Rules.Term |
| checkpoint | Mikan.TypeChecking.Monad.Context, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| CheckpointId | |
| 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 |
| checkpointSubstitution | Mikan.TypeChecking.Monad.Context, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| checkpointSubstitution' | Mikan.TypeChecking.Monad.Context, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| checkPositivity_ | Mikan.TypeChecking.Rules.Decl |
| CheckPragma | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| checkPragma | Mikan.TypeChecking.Rules.Decl |
| checkPragmaOptionConsistency | Mikan.TypeChecking.Monad.Options, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| CheckPrimitive | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| checkPrimitive | Mikan.TypeChecking.Rules.Decl |
| CheckProjAppToKnownPrincipalArg | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| checkProjAppToKnownPrincipalArg | Mikan.TypeChecking.Rules.Application |
| CheckProjection | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| checkProjectionLikeness_ | Mikan.TypeChecking.Rules.Decl |
| checkQuestionMark | Mikan.TypeChecking.Rules.Term |
| CheckRecDef | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| checkRecDef | Mikan.TypeChecking.Rules.Record |
| checkRecordExpression | Mikan.TypeChecking.Rules.Term |
| checkRecordProjections | Mikan.TypeChecking.Rules.Record |
| checkRecordUpdate | Mikan.TypeChecking.Rules.Term |
| checkRecordWhere | Mikan.TypeChecking.Rules.Term |
| CheckResult | |
| 1 (Type/Class) | Mikan.Interaction.Imports, Mikan.Compiler.Backend |
| 2 (Data Constructor) | Mikan.Interaction.Imports, Mikan.Compiler.Backend |
| CheckRHS | Mikan.Benchmarking, Mikan.TypeChecking.Monad.Benchmark |
| checkRHS | Mikan.TypeChecking.Rules.Def |
| checkSection | Mikan.TypeChecking.Rules.Decl |
| CheckSectionApplication | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| checkSectionApplication | Mikan.TypeChecking.Rules.Decl |
| checkSectionApplication' | Mikan.TypeChecking.Rules.Decl |
| checkSig | Mikan.TypeChecking.Rules.Decl |
| checkSolutionForMeta | Mikan.TypeChecking.MetaVars |
| checkSolved | Mikan.Mimer.Monad |
| checkSortOfSplitVar | Mikan.TypeChecking.Rules.LHS |
| checkStrictlyPositive | Mikan.TypeChecking.Positivity |
| checkSyntacticEquality | Mikan.TypeChecking.SyntacticEquality |
| checkSystemCoverage | Mikan.TypeChecking.Rules.Def |
| checkTacticAttribute | Mikan.TypeChecking.Rules.Term |
| CheckTargetType | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| checkTelePiSort | Mikan.TypeChecking.Sort |
| checkTelescope | Mikan.TypeChecking.Rules.Term |
| checkTelescope' | Mikan.TypeChecking.Rules.Term |
| checkTermination_ | Mikan.TypeChecking.Rules.Decl |
| CheckType | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| checkType | Mikan.TypeChecking.CheckInternal |
| checkTypeCheckingProblem | Mikan.TypeChecking.Constraints |
| checkTypedBindings | Mikan.TypeChecking.Rules.Term |
| checkTypeSignature | Mikan.TypeChecking.Rules.Decl |
| checkTypeSignature' | Mikan.TypeChecking.Rules.Decl |
| checkUnderscore | Mikan.TypeChecking.Rules.Term |
| checkUnquoteDecl | Mikan.TypeChecking.Rules.Decl |
| checkUnquoteDef | Mikan.TypeChecking.Rules.Decl |
| checkWhere | Mikan.TypeChecking.Rules.Def |
| CheckWithApp | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| CheckWithAppHead | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| checkWithAppHead | Mikan.TypeChecking.Rules.WithApp |
| checkWithApplication | Mikan.TypeChecking.Rules.WithApp |
| checkWithFunction | Mikan.TypeChecking.Rules.Def |
| CheckWithFunctionLet | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| CheckWithFunctionType | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| checkWithRHS | Mikan.TypeChecking.Rules.Def |
| choice | Mikan.TypeChecking.Unquote |
| ChooseEither | Mikan.TypeChecking.Rules.LHS.Problem |
| ChooseFlex | Mikan.TypeChecking.Rules.LHS.Problem |
| chooseFlex | Mikan.TypeChecking.Rules.LHS.Problem |
| chooseHighlightingMethod | Mikan.Interaction.Highlighting.Common |
| ChooseLeft | Mikan.TypeChecking.Rules.LHS.Problem |
| ChooseRight | Mikan.TypeChecking.Rules.LHS.Problem |
| choosing | Mikan.Utils.Lens, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| chop | Mikan.Utils.List |
| chopWhen | Mikan.Utils.List |
| chosen | Mikan.Utils.Lens, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| Chr | Mikan.Syntax.Common.Pretty |
| Cl | |
| 1 (Type/Class) | Mikan.TypeChecking.CompiledClause.Compile |
| 2 (Data Constructor) | Mikan.TypeChecking.CompiledClause.Compile |
| cl | Mikan.TypeChecking.Names |
| cl' | Mikan.TypeChecking.Names |
| ClashesViaRenaming | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| ClashesViaRenaming_ | Mikan.Interaction.Options.Warnings |
| ClashingAbstractName | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| ClashingDefinition | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| ClashingDefinition_ | Mikan.Interaction.Options.Errors |
| ClashingModule | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| ClashingModule_ | Mikan.Interaction.Options.Errors |
| ClashingName | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| ClashingQName | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| clashingQName | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| classifyBuiltinModule_ | Mikan.Interaction.Library |
| classifyWarning | Mikan.TypeChecking.Warnings |
| classifyWarnings | Mikan.TypeChecking.Warnings |
| Clause | |
| 1 (Type/Class) | Mikan.Syntax.Internal.Clause |
| 2 (Data Constructor) | Mikan.Syntax.Internal.Clause |
| 3 (Type/Class) | Mikan.Syntax.Reflected |
| 4 (Data Constructor) | Mikan.Syntax.Reflected |
| 5 (Type/Class) | Mikan.Syntax.Concrete.Definitions.Types, Mikan.Syntax.Concrete.Definitions |
| 6 (Data Constructor) | Mikan.Syntax.Concrete.Definitions.Types, Mikan.Syntax.Concrete.Definitions |
| 7 (Type/Class) | Mikan.Syntax.Abstract |
| 8 (Data Constructor) | Mikan.Syntax.Abstract |
| Clause' | Mikan.Syntax.Abstract |
| clauseArgs | Mikan.Syntax.Internal.Clause |
| clauseBody | Mikan.Syntax.Internal.Clause |
| clauseCatchall | |
| 1 (Function) | Mikan.Syntax.Internal.Clause |
| 2 (Function) | Mikan.Syntax.Abstract |
| clauseElims | Mikan.Syntax.Internal.Clause |
| clauseEllipsis | Mikan.Syntax.Internal.Clause |
| clauseFullRange | Mikan.Syntax.Internal.Clause |
| ClauseLHS | Mikan.TypeChecking.Rules.LHS |
| clauseLHS | Mikan.Syntax.Abstract |
| clauseLHSRange | Mikan.Syntax.Internal.Clause |
| ClauseNumber | Mikan.TypeChecking.CompiledClause |
| clausePats | |
| 1 (Function) | Mikan.Syntax.Internal.Clause |
| 2 (Function) | Mikan.Syntax.Reflected |
| clausePerm | Mikan.Syntax.Internal.Clause |
| ClauseRecursive | Mikan.Syntax.Internal.Clause |
| clauseRecursive | Mikan.Syntax.Internal.Clause |
| clauseRHS | |
| 1 (Function) | Mikan.Syntax.Reflected |
| 2 (Function) | Mikan.Syntax.Abstract |
| ClauseS | Mikan.Syntax.Abstract |
| ClauseSpine | Mikan.Syntax.Abstract |
| clauseSpine | Mikan.Syntax.Abstract |
| ClausesPostChecks | Mikan.TypeChecking.Rules.Def |
| clauseStrippedPats | Mikan.Syntax.Abstract |
| clauseTel | |
| 1 (Function) | Mikan.Syntax.Internal.Clause |
| 2 (Function) | Mikan.Syntax.Reflected |
| clauseToSplitClause | Mikan.TypeChecking.Coverage.SplitClause, Mikan.TypeChecking.Coverage |
| clauseType | Mikan.Syntax.Internal.Clause |
| clauseUnreachable | Mikan.Syntax.Internal.Clause |
| clauseWhereDecls | Mikan.Syntax.Abstract |
| clauseWhereModule | Mikan.Syntax.Internal.Clause |
| ClauseZipper | Mikan.Interaction.MakeCase |
| clBody | Mikan.TypeChecking.CompiledClause.Compile |
| Clean | Mikan.TypeChecking.Unquote |
| clean | Mikan.Utils.Graph.AdjacencyMap.Unidirectional |
| cleanCachedLog | Mikan.TypeChecking.Monad.Caching, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| clearMetaListeners | Mikan.TypeChecking.Monad.MetaVars, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| clearRunningInfo | Mikan.Interaction.EmacsCommand |
| clearUnknownInstance | Mikan.TypeChecking.Monad.State, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| clEnv | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| clModuleCheckpoints | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| clNumber | Mikan.TypeChecking.CompiledClause.Compile |
| clobberLiveNames | Mikan.Syntax.Scope.Trimming |
| ClockTime | Mikan.Utils.Time |
| clone | Mikan.Utils.HashTable |
| cloneIndexedLens | Mikan.Utils.Lens, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| cloneIndexedSetter | Mikan.Utils.Lens, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| cloneIndexedTraversal | Mikan.Utils.Lens, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| cloneIndexedTraversal1 | Mikan.Utils.Lens, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| cloneIndexPreservingLens | Mikan.Utils.Lens, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| cloneIndexPreservingSetter | Mikan.Utils.Lens, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| cloneIndexPreservingTraversal | Mikan.Utils.Lens, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| cloneIndexPreservingTraversal1 | Mikan.Utils.Lens, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| cloneIso | Mikan.Utils.Lens, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| cloneLens | Mikan.Utils.Lens, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| cloneSetter | Mikan.Utils.Lens, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| cloneTraversal | Mikan.Utils.Lens, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| cloneTraversal1 | Mikan.Utils.Lens, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| closeBracket | Mikan.Syntax.Parser.Monad |
| closed | Mikan.TypeChecking.Free |
| ClosedLevel | Mikan.Syntax.Internal.Term |
| ClosedType | Mikan.TypeChecking.Primitive.Cubical, Mikan.TypeChecking.Primitive |
| closeTwoBraces | Mikan.Syntax.Parser.Helpers |
| closeVerboseBracket | Mikan.TypeChecking.Monad.Debug, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| closeVerboseBracketException | Mikan.TypeChecking.Monad.Debug, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| Closure | |
| 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 |
| clPats | Mikan.TypeChecking.CompiledClause.Compile |
| clRecursive | Mikan.TypeChecking.CompiledClause.Compile |
| Cls | Mikan.TypeChecking.CompiledClause.Compile |
| clScope | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| clSignature | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| clValue | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| CMaybe | Mikan.Utils.Singleton |
| cMaybe | Mikan.Utils.Singleton |
| Cmd_abort | Mikan.Interaction.Base |
| Cmd_autoAll | Mikan.Interaction.Base |
| Cmd_autoOne | Mikan.Interaction.Base |
| Cmd_backend_hole | Mikan.Interaction.Base |
| Cmd_backend_top | Mikan.Interaction.Base |
| Cmd_compile | Mikan.Interaction.Base |
| Cmd_compute | Mikan.Interaction.Base |
| Cmd_compute_toplevel | Mikan.Interaction.Base |
| Cmd_constraints | Mikan.Interaction.Base |
| Cmd_context | Mikan.Interaction.Base |
| Cmd_elaborate_give | Mikan.Interaction.Base |
| Cmd_exit | Mikan.Interaction.Base |
| Cmd_give | Mikan.Interaction.Base |
| Cmd_goal_type | Mikan.Interaction.Base |
| Cmd_goal_type_context | Mikan.Interaction.Base |
| cmd_goal_type_context_and | Mikan.Interaction.InteractionTop |
| Cmd_goal_type_context_check | Mikan.Interaction.Base |
| Cmd_goal_type_context_infer | Mikan.Interaction.Base |
| Cmd_helper_function | Mikan.Interaction.Base |
| Cmd_highlight | Mikan.Interaction.Base |
| Cmd_infer | Mikan.Interaction.Base |
| Cmd_infer_toplevel | Mikan.Interaction.Base |
| Cmd_intro | Mikan.Interaction.Base |
| Cmd_load | Mikan.Interaction.Base |
| cmd_load' | Mikan.Interaction.InteractionTop |
| Cmd_load_highlighting_info | Mikan.Interaction.Base |
| Cmd_load_no_metas | Mikan.Interaction.Base |
| Cmd_make_case | Mikan.Interaction.Base |
| Cmd_metas | Mikan.Interaction.Base |
| Cmd_refine | Mikan.Interaction.Base |
| Cmd_refine_or_intro | Mikan.Interaction.Base |
| Cmd_search_about_toplevel | Mikan.Interaction.Base |
| Cmd_show_module_contents | Mikan.Interaction.Base |
| Cmd_show_module_contents_toplevel | Mikan.Interaction.Base |
| Cmd_show_version | Mikan.Interaction.Base |
| Cmd_solveAll | Mikan.Interaction.Base |
| Cmd_solveOne | Mikan.Interaction.Base |
| Cmd_tokenHighlighting | Mikan.Interaction.Base |
| Cmd_why_in_scope | Mikan.Interaction.Base |
| Cmd_why_in_scope_toplevel | Mikan.Interaction.Base |
| CmpElim | Mikan.Interaction.Base |
| CmpEq | Mikan.TypeChecking.Monad.Base.Types, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| CmpInType | Mikan.Interaction.Base |
| CmpLeq | Mikan.TypeChecking.Monad.Base.Types, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| CmpLevels | Mikan.Interaction.Base |
| CmpSorts | Mikan.Interaction.Base |
| CmpTeles | Mikan.Interaction.Base |
| CmpTypes | Mikan.Interaction.Base |
| CMSet | |
| 1 (Type/Class) | Mikan.Termination.CallMatrix |
| 2 (Data Constructor) | Mikan.Termination.CallMatrix |
| cmSet | Mikan.Termination.CallMatrix |
| CoConName | Mikan.Syntax.Abstract.Name, Mikan.Syntax.Internal.Term, Mikan.Syntax.Abstract |
| Code | Mikan.Syntax.Parser.Literate |
| code | Mikan.Syntax.Parser.Lexer |
| CoDomain | Mikan.Utils.TypeLevel |
| CoDomain' | Mikan.Utils.TypeLevel |
| CodomainNormalised | Mikan.TypeChecking.Substitute |
| CodomainNotNormalised | Mikan.TypeChecking.Substitute |
| codomainUniv | Mikan.Syntax.Internal.Univ, Mikan.Syntax.Internal.Term |
| coerce | Mikan.TypeChecking.Conversion |
| coerce' | Mikan.TypeChecking.Rules.Application |
| coerced | Mikan.Utils.Lens, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| coerceMeta | Mikan.TypeChecking.Conversion |
| CofUniv | Mikan.Syntax.Internal.Term |
| CoInductive | Mikan.Syntax.Common.Aspect, Mikan.Syntax.Common |
| CoinductiveDatatype | Mikan.TypeChecking.Coverage.Errors |
| CoinductiveDatatype_ | Mikan.Interaction.Options.Errors |
| CoinductiveEtaRecord | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| CoinductiveEtaRecord_ | Mikan.Interaction.Options.Warnings |
| Coinfective | Mikan.Interaction.Options |
| CoInfectiveImport | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| CoInfectiveImport_ | Mikan.Interaction.Options.Warnings |
| col | Mikan.Termination.SparseMatrix |
| ColdEnv | |
| 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 |
| collapseDefault | Mikan.Utils.WithDefault |
| Collect | Mikan.TypeChecking.Free.Generic |
| collectComponents | Mikan.Mimer.Monad |
| Collection | Mikan.Utils.Singleton |
| collectLHSVars | Mikan.Mimer.Monad |
| collectStats | Mikan.TypeChecking.Serialise.Base |
| colon | |
| 1 (Function) | Mikan.Syntax.Common.Pretty |
| 2 (Function) | Mikan.TypeChecking.Pretty |
| colorArg | Mikan.Interaction.Options.Arguments |
| colorValues | Mikan.Interaction.Options.Arguments |
| cols | Mikan.Termination.SparseMatrix |
| Column | Mikan.Syntax.Parser.Monad |
| ComatchingDisabledForRecord | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| ComatchingDisabledForRecord_ | Mikan.Interaction.Options.Errors |
| combineHashes | Mikan.Utils.Hash |
| combineInt | Mikan.Utils.Hash |
| combineSys | Mikan.TypeChecking.Primitive.Cubical.Base, Mikan.TypeChecking.Primitive.Cubical, Mikan.TypeChecking.Primitive |
| combineSys' | Mikan.TypeChecking.Primitive.Cubical.Base, Mikan.TypeChecking.Primitive.Cubical, Mikan.TypeChecking.Primitive |
| combineWord | Mikan.Utils.Hash |
| comma | |
| 1 (Function) | Mikan.Syntax.Common.Pretty |
| 2 (Function) | Mikan.TypeChecking.Pretty |
| Command | |
| 1 (Type/Class) | Mikan.Interaction.Base |
| 2 (Data Constructor) | Mikan.Interaction.Base |
| 3 (Type/Class) | Mikan.TypeChecking.Primitive.Cubical.Base, Mikan.TypeChecking.Primitive.Cubical, Mikan.TypeChecking.Primitive |
| Command' | Mikan.Interaction.Base |
| CommandError | Mikan.Interaction.ExitCode |
| commandLineFlags | Mikan.Compiler.Backend.Base, Mikan.Compiler.Backend |
| CommandLineOptions | Mikan.Interaction.Options |
| commandLineOptions | Mikan.Interaction.Options, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| CommandM | Mikan.Interaction.Command |
| CommandM' | Mikan.Interaction.Base |
| commandMToIO | Mikan.Interaction.InteractionTop |
| CommandPayload | Mikan.Compiler.Backend.Base, Mikan.Compiler.Backend |
| CommandQueue | |
| 1 (Type/Class) | Mikan.Interaction.Base |
| 2 (Data Constructor) | Mikan.Interaction.Base |
| commandQueue | Mikan.Interaction.Base |
| commands | Mikan.Interaction.Base |
| CommandState | |
| 1 (Type/Class) | Mikan.Interaction.Base |
| 2 (Data Constructor) | Mikan.Interaction.Base |
| Comment | |
| 1 (Data Constructor) | Mikan.Syntax.Common.Aspect, Mikan.Interaction.Highlighting.Precise |
| 2 (Data Constructor) | Mikan.Syntax.Parser.Literate |
| CommitAfterDef | Mikan.TypeChecking.Unquote.Errors |
| commitInfo | Mikan.VersionCommit |
| commonParentModule | Mikan.Syntax.Abstract.Name, Mikan.Syntax.Internal.Term, Mikan.Syntax.Abstract |
| commonPrefix | Mikan.Utils.List |
| commonSuffix | Mikan.Utils.List |
| Compact | Mikan.Utils.CompactRegion |
| compact | Mikan.Utils.CompactRegion |
| Compaction | Mikan.Benchmarking, Mikan.TypeChecking.Monad.Benchmark |
| compactP | Mikan.Utils.Permutation |
| Comparable | Mikan.Utils.PartialOrd |
| comparable | Mikan.Utils.PartialOrd |
| comparableOrd | Mikan.Utils.PartialOrd |
| Compare | Mikan.Benchmarking, Mikan.TypeChecking.Monad.Benchmark |
| compareArgs | Mikan.TypeChecking.Conversion |
| CompareAs | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| compareAs | Mikan.TypeChecking.Conversion |
| compareAs' | Mikan.TypeChecking.Conversion |
| compareAsDir | Mikan.TypeChecking.Conversion |
| compareAtom | Mikan.TypeChecking.Conversion |
| compareAtomDir | Mikan.TypeChecking.Conversion |
| CompareDirection | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| compareDom | Mikan.TypeChecking.Conversion |
| compareElims | Mikan.TypeChecking.Conversion |
| compareFavorites | Mikan.Utils.Favorites |
| compareInterval | Mikan.TypeChecking.Conversion |
| compareIrrelevant | Mikan.TypeChecking.Conversion |
| compareLength | Mikan.Utils.List1 |
| compareLevel | Mikan.TypeChecking.Conversion |
| compareMetas | Mikan.TypeChecking.Conversion |
| CompareResult | Mikan.Utils.Favorites |
| compareSort | Mikan.TypeChecking.Conversion |
| compareTerm | Mikan.TypeChecking.Conversion |
| compareTerm' | Mikan.TypeChecking.Conversion |
| compareTermOnFace | Mikan.TypeChecking.Conversion |
| compareTermOnFace' | Mikan.TypeChecking.Conversion |
| compareType | Mikan.TypeChecking.Conversion |
| compareWithFavorites | Mikan.Utils.Favorites |
| compareWithPol | Mikan.TypeChecking.Conversion |
| Comparison | Mikan.TypeChecking.Monad.Base.Types, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| compCost | Mikan.Mimer.Types |
| CompId | Mikan.Mimer.Types |
| compId | Mikan.Mimer.Types |
| CompilationError | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| CompilationError_ | Mikan.Interaction.Options.Errors |
| compile | Mikan.TypeChecking.CompiledClause.Compile |
| compileClauses | Mikan.TypeChecking.CompiledClause.Compile |
| compileClauses' | Mikan.TypeChecking.CompiledClause.Compile |
| compiledClauseBody | Mikan.TypeChecking.Substitute |
| CompiledClauses | Mikan.TypeChecking.CompiledClause |
| CompiledClauses' | Mikan.TypeChecking.CompiledClause |
| compileDef | Mikan.Compiler.Backend.Base, Mikan.Compiler.Backend |
| CompiledRepresentation | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| compileElispFiles | Mikan.Setup.EmacsMode |
| compileFlag | Mikan.Setup.EmacsMode |
| CompilePragma | |
| 1 (Data Constructor) | Mikan.Syntax.Concrete |
| 2 (Data Constructor) | Mikan.Syntax.Abstract |
| CompilerBackend | Mikan.Interaction.Base |
| CompilerPragma | |
| 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 |
| compileWithSplitTree | Mikan.TypeChecking.CompiledClause.Compile |
| CompKit | |
| 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 |
| complement | |
| 1 (Function) | Mikan.Utils.BoolSet |
| 2 (Function) | Mikan.Utils.VarSet |
| 3 (Function) | Mikan.Utils.SmallSet |
| complete | |
| 1 (Function) | Mikan.Utils.Graph.AdjacencyMap.Unidirectional |
| 2 (Function) | Mikan.Termination.CallGraph |
| 3 (Function) | Mikan.Interaction.Options.BashCompletion |
| completeIter | Mikan.Utils.Graph.AdjacencyMap.Unidirectional |
| Completion | |
| 1 (Type/Class) | Mikan.Interaction.Options.BashCompletion |
| 2 (Data Constructor) | Mikan.Interaction.Options.BashCompletion |
| completions | Mikan.Interaction.Options.BashCompletion |
| completionStep | Mikan.Termination.CallGraph |
| compMetas | Mikan.Mimer.Types |
| compName | Mikan.Mimer.Types |
| Component | |
| 1 (Type/Class) | Mikan.Mimer.Types |
| 2 (Data Constructor) | Mikan.Mimer.Types |
| ComponentCache | Mikan.Mimer.Types |
| composeFlexRig | Mikan.TypeChecking.Free.Base, Mikan.TypeChecking.Free |
| composeP | Mikan.Utils.Permutation |
| composePol | Mikan.TypeChecking.Polarity |
| composeRetract | Mikan.TypeChecking.Rules.LHS.Unify.LeftInverse |
| composeS | Mikan.TypeChecking.Substitute.Class, Mikan.TypeChecking.Substitute |
| composeVarOcc | Mikan.TypeChecking.Free.Base |
| composeWith | Mikan.Utils.Graph.AdjacencyMap.Unidirectional |
| ComposeZip | Mikan.Utils.Zipper |
| ComposeZipper | Mikan.Utils.Zipper |
| compPars | Mikan.Mimer.Types |
| compRec | Mikan.Mimer.Types |
| Compress | Mikan.Benchmarking, Mikan.TypeChecking.Monad.Benchmark |
| compress | Mikan.Utils.CompressedTrie |
| compTerm | Mikan.Mimer.Types |
| compType | Mikan.Mimer.Types |
| computeDefType | Mikan.TypeChecking.ProjectionLike |
| computeElimHeadType | Mikan.TypeChecking.Conversion |
| computeFixitiesAndPolarities | Mikan.Syntax.Scope.Monad |
| computeForcingAnnotations | Mikan.TypeChecking.Forcing |
| ComputeFree | Mikan.TypeChecking.Free.Generic |
| computeIgnoreAbstract | Mikan.Interaction.BasicOps |
| computeInCurrent | Mikan.Interaction.BasicOps |
| ComputeMode | Mikan.Interaction.Base |
| computeNodes | Mikan.Utils.Graph.AdjacencyMap.Unidirectional |
| computePolarity | Mikan.TypeChecking.Polarity |
| computeUnsolvedInfo | Mikan.Interaction.Highlighting.Generate |
| computeWrapInput | Mikan.Interaction.BasicOps |
| Con | |
| 1 (Data Constructor) | Mikan.Syntax.Internal.Term |
| 2 (Data Constructor) | Mikan.Syntax.Reflected |
| 3 (Data Constructor) | Mikan.Syntax.Abstract |
| conAbstr | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| conApp | Mikan.TypeChecking.Substitute |
| ConAppHd | Mikan.TypeChecking.Rules.Application |
| ConArgType | |
| 1 (Data Constructor) | Mikan.TypeChecking.Positivity.Occurrence |
| 2 (Data Constructor) | Mikan.TypeChecking.Positivity.Warnings |
| conArity | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| conBranches | Mikan.TypeChecking.CompiledClause |
| conCase | Mikan.TypeChecking.CompiledClause |
| concat | Mikan.Utils.List1 |
| concat' | |
| 1 (Function) | Mikan.Utils.List |
| 2 (Function) | Mikan.Utils.List1 |
| concat21 | Mikan.Utils.List2 |
| concatListT | Mikan.Utils.ListT |
| concatMap' | Mikan.Utils.List |
| concatMap1 | Mikan.Utils.List1 |
| concatMapM | Mikan.Utils.Monad |
| conComp | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| ConcreteDef | Mikan.Syntax.Common |
| ConcreteMode | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| ConcreteNames | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| concreteNamesInScope | Mikan.Syntax.Scope.Base |
| concreteToAbstract | Mikan.Syntax.Translation.ConcreteToAbstract |
| concreteToAbstract_ | Mikan.Syntax.Translation.ConcreteToAbstract |
| conData | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| conDataRecord | Mikan.Syntax.Abstract.Name, Mikan.Syntax.Internal.Term, Mikan.Syntax.Abstract |
| ConEndpoint | |
| 1 (Data Constructor) | Mikan.TypeChecking.Positivity.Occurrence |
| 2 (Data Constructor) | Mikan.TypeChecking.Positivity.Warnings |
| conFields | Mikan.Syntax.Abstract.Name, Mikan.Syntax.Internal.Term, Mikan.Syntax.Abstract |
| configAbove | Mikan.Interaction.Library.Base, Mikan.Interaction.Library |
| configAgdaLibFile | Mikan.Interaction.Library.Base, Mikan.Interaction.Library |
| configRoot | Mikan.Interaction.Library.Base, Mikan.Interaction.Library |
| Confirmed | Mikan.Syntax.Parser.Monad |
| confirmLayout | Mikan.Syntax.Parser.Layout |
| Conflict | Mikan.TypeChecking.Rules.LHS.Unify.Types |
| conflictAt | Mikan.TypeChecking.Rules.LHS.Unify.Types |
| conflictDatatype | Mikan.TypeChecking.Rules.LHS.Unify.Types |
| ConflictingPragmaOptions | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| ConflictingPragmaOptions_ | Mikan.Interaction.Options.Warnings |
| conflictLeft | Mikan.TypeChecking.Rules.LHS.Unify.Types |
| conflictParameters | Mikan.TypeChecking.Rules.LHS.Unify.Types |
| conflictRight | Mikan.TypeChecking.Rules.LHS.Unify.Types |
| conflictType | Mikan.TypeChecking.Rules.LHS.Unify.Types |
| conForced | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| confusing | Mikan.Utils.Lens, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| ConHead | |
| 1 (Type/Class) | Mikan.Syntax.Abstract.Name, Mikan.Syntax.Internal.Term, Mikan.Syntax.Abstract |
| 2 (Data Constructor) | Mikan.Syntax.Abstract.Name, Mikan.Syntax.Internal.Term, Mikan.Syntax.Abstract |
| conInductive | Mikan.Syntax.Abstract.Name, Mikan.Syntax.Internal.Term, Mikan.Syntax.Abstract |
| ConInfo | Mikan.Syntax.Internal.Term |
| conInline | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| ConInsteadOfDef | Mikan.TypeChecking.Unquote.Errors |
| Conj | Mikan.TypeChecking.Conversion |
| conKindOfName | Mikan.Syntax.Scope.Base |
| conKindOfName' | Mikan.Syntax.Scope.Base |
| conLikeNameKinds | Mikan.Syntax.Scope.Base |
| ConName | Mikan.Syntax.Abstract.Name, Mikan.Syntax.Internal.Term, Mikan.Syntax.Abstract |
| conName | Mikan.Syntax.Abstract.Name, Mikan.Syntax.Internal.Term, Mikan.Syntax.Abstract |
| connectInteractionPoint | Mikan.TypeChecking.Monad.MetaVars, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| ConOCon | Mikan.Syntax.Common |
| ConOfAbs | Mikan.Syntax.Translation.AbstractToConcrete |
| ConORec | Mikan.Syntax.Common |
| ConORecWhere | Mikan.Syntax.Common |
| ConOrigin | Mikan.Syntax.Common |
| ConOSplit | Mikan.Syntax.Common |
| ConOSystem | Mikan.Syntax.Common |
| ConP | |
| 1 (Data Constructor) | Mikan.Syntax.Internal.Pattern |
| 2 (Data Constructor) | Mikan.Syntax.Reflected |
| 3 (Data Constructor) | Mikan.Syntax.Abstract |
| conPars | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| ConPatEager | Mikan.Syntax.Info |
| ConPatInfo | |
| 1 (Type/Class) | Mikan.Syntax.Info |
| 2 (Data Constructor) | Mikan.Syntax.Info |
| conPatInfo | Mikan.Syntax.Info |
| ConPatLazy | |
| 1 (Type/Class) | Mikan.Syntax.Info |
| 2 (Data Constructor) | Mikan.Syntax.Info |
| conPatLazy | Mikan.Syntax.Info |
| conPatOrigin | Mikan.Syntax.Info |
| ConPatternInfo | |
| 1 (Type/Class) | Mikan.Syntax.Internal.Pattern |
| 2 (Data Constructor) | Mikan.Syntax.Internal.Pattern |
| conPFallThrough | Mikan.Syntax.Internal.Pattern |
| conPInfo | Mikan.Syntax.Internal.Pattern |
| conPLazy | Mikan.Syntax.Internal.Pattern |
| conPRecord | Mikan.Syntax.Internal.Pattern |
| conProj | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| conPType | Mikan.Syntax.Internal.Pattern |
| Cons | |
| 1 (Data Constructor) | Mikan.Utils.IndexedList |
| 2 (Data Constructor) | Mikan.Interaction.Emacs.Lisp |
| 3 (Data Constructor) | Mikan.TypeChecking.Serialise.Instances.General |
| 4 (Data Constructor) | Mikan.TypeChecking.Serialise.Instances.Highlighting |
| cons | |
| 1 (Function) | Mikan.Utils.List1 |
| 2 (Function) | Mikan.Utils.List2 |
| consecutiveAndSeparated | Mikan.Syntax.Position |
| ConsHead | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| consListT | Mikan.Utils.ListT |
| ConsMap0 | Mikan.Utils.TypeLevel |
| ConsMap1 | Mikan.Utils.TypeLevel |
| consMListT | Mikan.Utils.ListT |
| consOfHIT | Mikan.TypeChecking.Datatypes |
| conSrcCon | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| consS | Mikan.TypeChecking.Substitute.Class, Mikan.TypeChecking.Substitute |
| Const | |
| 1 (Type/Class) | Mikan.Utils.Lens, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| 2 (Data Constructor) | Mikan.Utils.Lens, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| Constant | Mikan.Utils.TypeLevel |
| Constant0 | Mikan.Utils.TypeLevel |
| Constant1 | Mikan.Utils.TypeLevel |
| ConstK | Mikan.TypeChecking.DiscrimTree.Types |
| Constr | |
| 1 (Type/Class) | Mikan.Syntax.Common |
| 2 (Data Constructor) | Mikan.Syntax.Common |
| constrainedPrims | Mikan.TypeChecking.Monad.Builtin, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| Constraint | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| constraintMetas | Mikan.TypeChecking.Monad.MetaVars, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| constraintProblems | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| Constraints | |
| 1 (Data Constructor) | Mikan.Interaction.Options.ProfileOptions |
| 2 (Type/Class) | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| ConstraintStatus | Mikan.TypeChecking.Monad.Constraints, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| constraintUnblocker | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| ConstrOfNonRecord | Mikan.Syntax.Scope.Base |
| Constructor | |
| 1 (Data Constructor) | Mikan.Syntax.Common.Aspect, Mikan.Interaction.Highlighting.Precise |
| 2 (Data Constructor) | Mikan.Syntax.Concrete |
| 3 (Type/Class) | Mikan.Syntax.Abstract |
| 4 (Data Constructor) | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| ConstructorBlock | Mikan.Syntax.Concrete.Definitions.Types |
| ConstructorData | |
| 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 |
| ConstructorDefn | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| ConstructorDisambiguationData | |
| 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 |
| ConstructorDoesNotFitInData | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| ConstructorDoesNotFitInData_ | Mikan.Interaction.Options.Warnings |
| ConstructorDoesNotTargetGivenType | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| ConstructorDoesNotTargetGivenType_ | Mikan.Interaction.Options.Errors |
| constructorFlexRig | Mikan.TypeChecking.Free.Base |
| constructorForm | Mikan.TypeChecking.Monad.Builtin, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| constructorForm' | Mikan.TypeChecking.Monad.Builtin, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| constructorFormer | Mikan.TypeChecking.Monad.Builtin, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| ConstructorInfo | Mikan.TypeChecking.Datatypes |
| ConstructorName | Mikan.Syntax.Scope.Base |
| ConstructorNameOfNonRecord | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| ConstructorNameOfNonRecord_ | Mikan.Interaction.Options.Errors |
| ConstructorOrPatternSynonym | Mikan.Syntax.Common |
| constructorOrPatternSynonymNameString | Mikan.Interaction.Options.Errors |
| ConstructorPatternInWrongDatatype | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| ConstructorPatternInWrongDatatype_ | Mikan.Interaction.Options.Errors |
| constructorTagModifier | Mikan.Interaction.JSON |
| constructs | Mikan.TypeChecking.Rules.Data |
| constTranspAxiom | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| Contains | Mikan.Utils.Lens, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| contains | Mikan.Utils.Lens, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| containsAbsurdPattern | Mikan.Syntax.Abstract.Pattern |
| containsAPattern | Mikan.Syntax.Abstract.Pattern |
| containsAsPattern | Mikan.Syntax.Abstract.Pattern |
| containsProfileOption | Mikan.Interaction.Options.ProfileOptions |
| content | Mikan.TypeChecking.CompiledClause |
| contentsFieldName | Mikan.Interaction.JSON |
| ContentWithoutField | Mikan.Interaction.Library.Base |
| Context | |
| 1 (Type/Class) | Mikan.TypeChecking.Monad.Base.Types, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| 2 (Data Constructor) | Mikan.TypeChecking.Monad.Base.Types, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| Context' | Mikan.TypeChecking.Monad.Base.Types, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| contextArgs | Mikan.TypeChecking.Monad.Context, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| ContextEntry | Mikan.TypeChecking.Monad.Base.Types, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| ContextLet | Mikan.Interaction.Base |
| contextNames | Mikan.TypeChecking.Monad.Context, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| contextNames' | Mikan.TypeChecking.Monad.Context, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| contextOfMeta | Mikan.Interaction.BasicOps |
| contextTerms | Mikan.TypeChecking.Monad.Context, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| contextToTel | Mikan.TypeChecking.Monad.Context, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| ContextVar | Mikan.Interaction.Base |
| contextVars | Mikan.TypeChecking.Monad.Context, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| contextVars' | Mikan.TypeChecking.Monad.Context, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| continuous | Mikan.Syntax.Position |
| continuousPerLine | Mikan.Syntax.Position |
| contramap | Mikan.Utils.Lens, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| contramapped | Mikan.Utils.Lens, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| contramapping | Mikan.Utils.Lens, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| Contravariant | |
| 1 (Type/Class) | Mikan.Utils.Lens, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| 2 (Data Constructor) | Mikan.TypeChecking.Monad.Base.Types, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| ConvApply | Mikan.TypeChecking.Conversion.Errors |
| ConvCod | Mikan.TypeChecking.Conversion.Errors |
| ConvDom | Mikan.TypeChecking.Conversion.Errors |
| convErrCmp | Mikan.TypeChecking.Conversion.Errors |
| convErrCtx | Mikan.TypeChecking.Conversion.Errors |
| convErrLhs | Mikan.TypeChecking.Conversion.Errors |
| convErrRhs | Mikan.TypeChecking.Conversion.Errors |
| convErrTys | Mikan.TypeChecking.Conversion.Errors |
| Conversion | Mikan.Interaction.Options.ProfileOptions |
| ConversionError | |
| 1 (Type/Class) | Mikan.TypeChecking.Conversion.Errors |
| 2 (Data Constructor) | Mikan.TypeChecking.Conversion.Errors |
| ConversionErrorContext | Mikan.TypeChecking.Conversion.Errors |
| ConversionFail | Mikan.Syntax.Common |
| ConversionZipper | Mikan.TypeChecking.Conversion.Errors |
| Convert | Mikan.Interaction.Highlighting.Precise |
| convert | Mikan.Interaction.Highlighting.Precise |
| ConvLam | Mikan.TypeChecking.Conversion.Errors |
| ConvStop | Mikan.TypeChecking.Conversion.Errors |
| CopatternHeadNotProjection | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| CopatternHeadNotProjection_ | Mikan.Interaction.Options.Errors |
| CopatternMatching | Mikan.Syntax.Common |
| CopatternMatchingAllowed | Mikan.Syntax.Common |
| copatternMatchingAllowed | Mikan.Syntax.Common |
| CopatternReductions | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| CopatternsNotAllowed | Mikan.Interaction.Options.Errors, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| copyBytes | Mikan.Utils.ShortText |
| copyDirContent | Mikan.Utils.IO.Directory |
| copyIfChanged | Mikan.Utils.IO.Directory |
| copyName | Mikan.Syntax.Scope.Trimming |
| copyScope | Mikan.Syntax.Scope.Monad |
| copyTerm | Mikan.Syntax.Internal.Generic |
| CosmeticProblem | Mikan.Syntax.Common.Aspect, Mikan.Interaction.Highlighting.Precise |
| CosplitNoRecordType | Mikan.TypeChecking.Coverage.Errors |
| CosplitNoRecordType_ | Mikan.Interaction.Options.Errors |
| CosplitNoTarget | Mikan.TypeChecking.Coverage.Errors |
| CosplitNoTarget_ | Mikan.Interaction.Options.Errors |
| Cost | Mikan.Mimer.Types |
| costAxiom | Mikan.Mimer.Types |
| costCompReuse | Mikan.Mimer.Types |
| costDataCon | Mikan.Mimer.Types |
| costFn | Mikan.Mimer.Types |
| costLet | Mikan.Mimer.Types |
| costLevel | Mikan.Mimer.Types |
| costLocal | Mikan.Mimer.Types |
| costNewHiddenMeta | Mikan.Mimer.Types |
| costNewMeta | Mikan.Mimer.Types |
| costProj | Mikan.Mimer.Types |
| costRecCall | Mikan.Mimer.Types |
| costRecordCon | Mikan.Mimer.Types |
| Costs | |
| 1 (Type/Class) | Mikan.Mimer.Types |
| 2 (Data Constructor) | Mikan.Mimer.Types |
| costSet | Mikan.Mimer.Types |
| costSpeculateProj | Mikan.Mimer.Types |
| CouldBeProjectionPattern | Mikan.Syntax.Concrete |
| couldBeRecursive | Mikan.Syntax.Internal.Clause |
| CountPatternVars | Mikan.Syntax.Internal.Pattern |
| countPatternVars | Mikan.Syntax.Internal.Pattern |
| countWithArgs | Mikan.TypeChecking.With |
| countWithPats | Mikan.TypeChecking.With |
| Covariant | Mikan.TypeChecking.Monad.Base.Types, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| Coverage | Mikan.Benchmarking, Mikan.TypeChecking.Monad.Benchmark |
| CoverageCheck | Mikan.Syntax.Common |
| coverageCheck | |
| 1 (Function) | Mikan.Syntax.Concrete.Definitions.Types |
| 2 (Function) | Mikan.TypeChecking.Coverage |
| coverageCheckPragma | Mikan.Syntax.Concrete.Definitions.Monad |
| CoverageIssue | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| CoverageIssue_ | Mikan.Interaction.Options.Warnings |
| CoverageNoExactSplit | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| CoverageNoExactSplit_ | Mikan.Interaction.Options.Warnings |
| CoverageProblem | Mikan.Syntax.Common.Aspect, Mikan.Interaction.Highlighting.Precise |
| Covering | |
| 1 (Type/Class) | Mikan.TypeChecking.Coverage.SplitClause, Mikan.TypeChecking.Coverage |
| 2 (Data Constructor) | Mikan.TypeChecking.Coverage.SplitClause, Mikan.TypeChecking.Coverage |
| coveringRange | Mikan.Utils.RangeMap, Mikan.Interaction.Highlighting.Precise |
| coverMissingClauses | Mikan.TypeChecking.Coverage.SplitClause |
| coverNoExactClauses | Mikan.TypeChecking.Coverage.SplitClause |
| coverPatterns | Mikan.TypeChecking.Coverage.SplitClause |
| CoverResult | |
| 1 (Type/Class) | Mikan.TypeChecking.Coverage.SplitClause |
| 2 (Data Constructor) | Mikan.TypeChecking.Coverage.SplitClause |
| coverSplitTree | Mikan.TypeChecking.Coverage.SplitClause |
| coverUsedClauses | Mikan.TypeChecking.Coverage.SplitClause |
| covFillTele | Mikan.TypeChecking.Coverage.Cubical |
| covSplitArg | Mikan.TypeChecking.Coverage.SplitClause, Mikan.TypeChecking.Coverage |
| covSplitClauses | Mikan.TypeChecking.Coverage.SplitClause, Mikan.TypeChecking.Coverage |
| CPatternLike | Mikan.Syntax.Concrete.Pattern |
| CPC | Mikan.TypeChecking.Rules.Def |
| cpcPartialSplits | Mikan.TypeChecking.Rules.Def |
| CPUTime | |
| 1 (Type/Class) | Mikan.Utils.Time |
| 2 (Data Constructor) | Mikan.Utils.Time |
| createMeta | Mikan.Mimer.Monad |
| createMetaInfo | Mikan.TypeChecking.Monad.MetaVars, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| createMetaInfo' | Mikan.TypeChecking.Monad.MetaVars, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| createMissingHCompClause | Mikan.TypeChecking.Coverage.Cubical |
| createMissingIndexedClauses | Mikan.TypeChecking.Coverage.Cubical |
| createMissingTrXConClause | Mikan.TypeChecking.Coverage.Cubical |
| createMissingTrXHCompClause | Mikan.TypeChecking.Coverage.Cubical |
| createMissingTrXTrXClause | Mikan.TypeChecking.Coverage.Cubical |
| createModule | Mikan.Syntax.Scope.Monad |
| crInterface | Mikan.Interaction.Imports, Mikan.Compiler.Backend |
| crMode | Mikan.Interaction.Imports, Mikan.Compiler.Backend |
| crModuleInfo | Mikan.Interaction.Imports |
| crSource | Mikan.Interaction.Imports |
| crWarnings | Mikan.Interaction.Imports, Mikan.Compiler.Backend |
| ctxEntryDom | Mikan.TypeChecking.Monad.Context, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| ctxEntryName | Mikan.TypeChecking.Monad.Context, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| ctxEntryType | Mikan.TypeChecking.Monad.Context, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| CtxVar | Mikan.TypeChecking.Monad.Base.Types, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| CType | Mikan.TypeChecking.Primitive.Cubical, Mikan.TypeChecking.Primitive |
| CubicalLeftInversion | Mikan.Benchmarking, Mikan.TypeChecking.Monad.Benchmark |
| cubicalPrimChecks | Mikan.TypeChecking.Rules.Cubical |
| CubicalPrimitiveNotFullyApplied | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| CubicalPrimitiveNotFullyApplied_ | Mikan.Interaction.Options.Errors |
| curDefs | Mikan.Compiler.Common |
| curIF | Mikan.Compiler.Common |
| curMName | Mikan.Compiler.Common |
| CurrentAccount | Mikan.Utils.Benchmark |
| currentAccount | Mikan.Utils.Benchmark |
| currentCxt | Mikan.TypeChecking.Names |
| CurrentFile | |
| 1 (Type/Class) | Mikan.Interaction.Base |
| 2 (Data Constructor) | Mikan.Interaction.Base |
| currentFileArgs | Mikan.Interaction.Base |
| currentFileModule | Mikan.Interaction.Base |
| currentFilePath | Mikan.Interaction.Base |
| currentFileStamp | Mikan.Interaction.Base |
| CurrentInput | Mikan.Syntax.Parser.Alex |
| currentModule | Mikan.TypeChecking.Monad.Env, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| currentModuleNameHash | Mikan.TypeChecking.Monad.State, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| currentOrFreshMutualBlock | Mikan.TypeChecking.Monad.Mutual, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| currentTopLevelModule | Mikan.TypeChecking.Monad.State, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| CurrentTypeCheckLog | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| curried | Mikan.Utils.Lens, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| curry | Mikan.Utils.Tuple.Strict |
| curryAt | Mikan.TypeChecking.Records |
| Currying | Mikan.Utils.TypeLevel |
| currys | Mikan.Utils.TypeLevel |
| CustomBackendError | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| CustomBackendError_ | Mikan.Interaction.Options.Errors |
| CustomBackendWarning | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| CustomBackendWarning_ | Mikan.Interaction.Options.Warnings |
| customCosts | Mikan.Mimer.Monad |
| cutConversionErrors | Mikan.TypeChecking.Conversion.Errors |
| CutOff | |
| 1 (Type/Class) | Mikan.Termination.CutOff |
| 2 (Data Constructor) | Mikan.Termination.CutOff |
| cxDrop | Mikan.TypeChecking.Monad.Base.Types, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| CxEmpty | Mikan.TypeChecking.Monad.Base.Types, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| cxEntries | Mikan.TypeChecking.Monad.Base.Types, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| CxExtend | Mikan.TypeChecking.Monad.Base.Types, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| CxExtendVar | Mikan.TypeChecking.Monad.Base.Types, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| cxLookup | Mikan.TypeChecking.Monad.Base.Types, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| cxPrepend | Mikan.TypeChecking.Monad.Base.Types, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| cxSplitAt | Mikan.TypeChecking.Monad.Base.Types, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| cxTake | Mikan.TypeChecking.Monad.Base.Types, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| cxtSubst | Mikan.TypeChecking.Names |
| cxWithIndex | Mikan.TypeChecking.Monad.Base.Types, Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| cycle | |
| 1 (Function) | Mikan.Utils.List1 |
| 2 (Function) | Mikan.Utils.ListInf |
| CyclicModuleDependency | Mikan.TypeChecking.Monad.Base, Mikan.TypeChecking.Monad, Mikan.Compiler.Backend |
| CyclicModuleDependency_ | Mikan.Interaction.Options.Errors |