| addUnusedTopVals | Ide.Plugin.Tactic.CodeGen |
| AgdaMatch | |
| 1 (Type/Class) | Ide.Plugin.Tactic.Types |
| 2 (Data Constructor) | Ide.Plugin.Tactic.Types |
| algebraicTyCon | Ide.Plugin.Tactic.GHC |
| allFeatures | Ide.Plugin.Tactic.FeatureSet |
| allNames | Ide.Plugin.Tactic.Tactics |
| allOccNames | Ide.Plugin.Tactic.GHC |
| AlreadyDestructed | Ide.Plugin.Tactic.Types |
| amBody | Ide.Plugin.Tactic.Types |
| amPats | Ide.Plugin.Tactic.Types |
| appDollar | Ide.Plugin.Tactic.CodeGen.Utils, Ide.Plugin.Tactic.CodeGen |
| apply | Ide.Plugin.Tactic.Tactics |
| assoc23 | Ide.Plugin.Tactic.Machinery |
| assume | Ide.Plugin.Tactic.Tactics |
| assumption | Ide.Plugin.Tactic.Tactics |
| attemptOn | Ide.Plugin.Tactic.Tactics |
| Auto | Ide.Plugin.Tactic.TestTypes, Ide.Plugin.Tactic |
| auto | Ide.Plugin.Tactic.Auto |
| auto' | Ide.Plugin.Tactic.Tactics |
| blacklistingDestruct | Ide.Plugin.Tactic.Judgements |
| buildDataCon | Ide.Plugin.Tactic.CodeGen |
| bvar' | Ide.Plugin.Tactic.CodeGen.Utils, Ide.Plugin.Tactic.CodeGen |
| CantHaveAnEmptyDataType | Ide.Plugin.Tactic.FeatureSet |
| Case | Ide.Plugin.Tactic.GHC |
| cfg_feature_set | Ide.Plugin.Tactic.TestTypes |
| ClassMethodPrv | Ide.Plugin.Tactic.Types |
| cloneTyVar | Ide.Plugin.Tactic.GHC |
| coerceName | Ide.Plugin.Tactic.CodeGen.Utils, Ide.Plugin.Tactic.CodeGen |
| commandProvider | Ide.Plugin.Tactic.LanguageServer.TacticProviders |
| commandTactic | Ide.Plugin.Tactic.LanguageServer.TacticProviders |
| Config | |
| 1 (Type/Class) | Ide.Plugin.Tactic.TestTypes |
| 2 (Data Constructor) | Ide.Plugin.Tactic.TestTypes |
| containsHole | Ide.Plugin.Tactic.GHC |
| containsHsVar | Ide.Plugin.Tactic.GHC |
| Context | |
| 1 (Type/Class) | Ide.Plugin.Tactic.Types |
| 2 (Data Constructor) | Ide.Plugin.Tactic.Types |
| contextMethodHypothesis | Ide.Plugin.Tactic.Context |
| countRecursiveCall | Ide.Plugin.Tactic.CodeGen |
| ctxDefiningFuncs | Ide.Plugin.Tactic.Types |
| ctxFeatureSet | Ide.Plugin.Tactic.Types |
| ctxModuleFuncs | Ide.Plugin.Tactic.Types |
| CType | |
| 1 (Type/Class) | Ide.Plugin.Tactic.Types |
| 2 (Data Constructor) | Ide.Plugin.Tactic.Types |
| dataConExTys | Ide.Plugin.Tactic.GHC |
| dataConInstOrigArgTys' | Ide.Plugin.Tactic.CodeGen |
| defaultFeatures | Ide.Plugin.Tactic.FeatureSet |
| defaultTacticState | Ide.Plugin.Tactic.Types |
| definedThetaType | Ide.Plugin.Tactic.Context |
| deriveArbitrary | Ide.Plugin.Tactic.KnownStrategies.QuickCheck |
| deriveFmap | Ide.Plugin.Tactic.KnownStrategies |
| descriptor | Ide.Plugin.Tactic |
| Destruct | Ide.Plugin.Tactic.TestTypes, Ide.Plugin.Tactic |
| destruct | Ide.Plugin.Tactic.Tactics |
| destruct' | Ide.Plugin.Tactic.CodeGen |
| destructAuto | Ide.Plugin.Tactic.Tactics |
| DestructLambdaCase | Ide.Plugin.Tactic.TestTypes, Ide.Plugin.Tactic |
| destructLambdaCase | Ide.Plugin.Tactic.Tactics |
| destructLambdaCase' | Ide.Plugin.Tactic.CodeGen |
| destructMatches | Ide.Plugin.Tactic.CodeGen |
| DisallowedPrv | Ide.Plugin.Tactic.Types |
| disallowing | Ide.Plugin.Tactic.Judgements |
| DisallowReason | Ide.Plugin.Tactic.Types |
| doesTypeContain | Ide.Plugin.Tactic.KnownStrategies.QuickCheck |
| dropEveryOther | Ide.Plugin.Tactic.Types |
| emptyConfig | Ide.Plugin.Tactic.TestTypes |
| emptyContext | Ide.Plugin.Tactic.Types |
| eqRdrName | Ide.Plugin.Tactic.GHC |
| excludeForbiddenMethods | Ide.Plugin.Tactic.Context |
| ExtractM | |
| 1 (Type/Class) | Ide.Plugin.Tactic.Types |
| 2 (Data Constructor) | Ide.Plugin.Tactic.Types |
| Feature | Ide.Plugin.Tactic.FeatureSet |
| FeatureSet | Ide.Plugin.Tactic.FeatureSet |
| filterPosition | Ide.Plugin.Tactic.Judgements |
| filterReplace | Ide.Plugin.Tactic.Naming |
| filterSameTypeFromOtherPositions | Ide.Plugin.Tactic.Judgements |
| freshTyvars | Ide.Plugin.Tactic.GHC |
| freshUnique | Ide.Plugin.Tactic.Types |
| fromPatCompatPs | Ide.Plugin.Tactic.GHC |
| fromPatCompatTc | Ide.Plugin.Tactic.GHC |
| Generator | |
| 1 (Type/Class) | Ide.Plugin.Tactic.KnownStrategies.QuickCheck |
| 2 (Data Constructor) | Ide.Plugin.Tactic.KnownStrategies.QuickCheck |
| genExpr | Ide.Plugin.Tactic.KnownStrategies.QuickCheck |
| genRecursiveCount | Ide.Plugin.Tactic.KnownStrategies.QuickCheck |
| getCurrentDefinitions | Ide.Plugin.Tactic.Context |
| getFeatureSet | Ide.Plugin.Tactic.LanguageServer |
| getFunBindId | Ide.Plugin.Tactic.Context |
| getIdeDynflags | Ide.Plugin.Tactic.LanguageServer |
| getInScope | Ide.Plugin.Tactic.Naming |
| getModuleHypothesis | Ide.Plugin.Tactic.Context |
| getPatName | Ide.Plugin.Tactic.GHC |
| getRecordFields | Ide.Plugin.Tactic.GHC |
| getRhsPosVals | Ide.Plugin.Tactic.LanguageServer |
| getSpanAndTypeAtHole | Ide.Plugin.Tactic.LanguageServer |
| getViaUnique | Ide.Plugin.Tactic.Types |
| GoalMismatch | Ide.Plugin.Tactic.Types |
| guardStructurallySmallerRecursion | Ide.Plugin.Tactic.Machinery |
| hasFeature | Ide.Plugin.Tactic.FeatureSet |
| hi_name | Ide.Plugin.Tactic.Types |
| hi_provenance | Ide.Plugin.Tactic.Types |
| hi_type | Ide.Plugin.Tactic.Types |
| homo | Ide.Plugin.Tactic.Tactics |
| homoLambdaCase | Ide.Plugin.Tactic.Tactics |
| Homomorphism | Ide.Plugin.Tactic.TestTypes, Ide.Plugin.Tactic |
| HomomorphismLambdaCase | Ide.Plugin.Tactic.TestTypes, Ide.Plugin.Tactic |
| hyByName | Ide.Plugin.Tactic.Judgements |
| HyInfo | |
| 1 (Type/Class) | Ide.Plugin.Tactic.Types |
| 2 (Data Constructor) | Ide.Plugin.Tactic.Types |
| hyNamesInScope | Ide.Plugin.Tactic.Judgements |
| Hypothesis | |
| 1 (Type/Class) | Ide.Plugin.Tactic.Types |
| 2 (Data Constructor) | Ide.Plugin.Tactic.Types |
| hypothesisFromBindings | Ide.Plugin.Tactic.Judgements |
| IncorrectDataCon | Ide.Plugin.Tactic.Types |
| infixCall | Ide.Plugin.Tactic.CodeGen.Utils, Ide.Plugin.Tactic.CodeGen |
| infixifyPatIfNecessary | Ide.Plugin.Tactic.CodeGen |
| instantiateType | Ide.Plugin.Tactic.GHC |
| introducingLambda | Ide.Plugin.Tactic.Judgements |
| introducingPat | Ide.Plugin.Tactic.Judgements |
| introducingRecursively | Ide.Plugin.Tactic.Judgements |
| Intros | Ide.Plugin.Tactic.TestTypes, Ide.Plugin.Tactic |
| intros | Ide.Plugin.Tactic.Tactics |
| isDestructBlacklisted | Ide.Plugin.Tactic.Judgements |
| isFunction | Ide.Plugin.Tactic.GHC |
| isHole | Ide.Plugin.Tactic.GHC |
| isPatternMatch | Ide.Plugin.Tactic.Judgements |
| isRhsHole | Ide.Plugin.Tactic.LanguageServer |
| isSplitWhitelisted | Ide.Plugin.Tactic.Judgements |
| isTopHole | Ide.Plugin.Tactic.Judgements |
| isTopLevel | Ide.Plugin.Tactic.Judgements |
| iterateSplit | Ide.Plugin.Tactic.CaseSplit |
| jEntireHypothesis | Ide.Plugin.Tactic.Judgements |
| jGoal | Ide.Plugin.Tactic.Judgements |
| jHypothesis | Ide.Plugin.Tactic.Judgements |
| jLocalHypothesis | Ide.Plugin.Tactic.Judgements |
| jPatHypothesis | Ide.Plugin.Tactic.Judgements |
| Judgement | |
| 1 (Type/Class) | Ide.Plugin.Tactic.Types |
| 2 (Data Constructor) | Ide.Plugin.Tactic.Types |
| Judgement' | Ide.Plugin.Tactic.Types |
| judgementForHole | Ide.Plugin.Tactic.LanguageServer |
| known | Ide.Plugin.Tactic.KnownStrategies |
| knownStrategies | Ide.Plugin.Tactic.KnownStrategies |
| Lambda | Ide.Plugin.Tactic.GHC |
| lambdaCaseable | Ide.Plugin.Tactic.GHC |
| liftMaybe | Ide.Plugin.Tactic.LanguageServer |
| localTactic | Ide.Plugin.Tactic.Tactics |
| markStructuralySmallerRecursion | Ide.Plugin.Tactic.Machinery |
| matching | Ide.Plugin.Tactic.Tactics |
| methodHypothesis | Ide.Plugin.Tactic.Machinery |
| mkArbitraryCall | Ide.Plugin.Tactic.KnownStrategies.QuickCheck |
| mkCon | Ide.Plugin.Tactic.CodeGen.Utils, Ide.Plugin.Tactic.CodeGen |
| mkContext | Ide.Plugin.Tactic.Context |
| mkDestructPat | Ide.Plugin.Tactic.CodeGen |
| mkFirstAgda | Ide.Plugin.Tactic.CaseSplit |
| mkFirstJudgement | Ide.Plugin.Tactic.Judgements |
| mkFunc | Ide.Plugin.Tactic.CodeGen.Utils, Ide.Plugin.Tactic.CodeGen |
| mkGenerator | Ide.Plugin.Tactic.KnownStrategies.QuickCheck |
| mkGoodName | Ide.Plugin.Tactic.Naming |
| mkJudgementAndContext | Ide.Plugin.Tactic.LanguageServer |
| mkManyGoodNames | Ide.Plugin.Tactic.Naming |
| mkTyConName | Ide.Plugin.Tactic.Naming |
| mkTyName | Ide.Plugin.Tactic.Naming |
| mkVal | Ide.Plugin.Tactic.CodeGen.Utils, Ide.Plugin.Tactic.CodeGen |
| Name | Ide.Plugin.Tactic.Types |
| newSubgoal | Ide.Plugin.Tactic.Machinery |
| NoApplicableTactic | Ide.Plugin.Tactic.Types |
| NoProgress | Ide.Plugin.Tactic.Types |
| NotInScope | Ide.Plugin.Tactic.Types |
| OccName | Ide.Plugin.Tactic.Types |
| overAlgebraicTerms | Ide.Plugin.Tactic.Tactics |
| overFunctions | Ide.Plugin.Tactic.Tactics |
| overProvenance | Ide.Plugin.Tactic.Types |
| parseFeatureSet | Ide.Plugin.Tactic.FeatureSet |
| PatCompat | Ide.Plugin.Tactic.GHC |
| PatternMatchPrv | Ide.Plugin.Tactic.Types |
| PatVal | |
| 1 (Type/Class) | Ide.Plugin.Tactic.Types |
| 2 (Data Constructor) | Ide.Plugin.Tactic.Types |
| Penalize | |
| 1 (Type/Class) | Ide.Plugin.Tactic.Machinery |
| 2 (Data Constructor) | Ide.Plugin.Tactic.Machinery |
| popRecursionStack | Ide.Plugin.Tactic.Types |
| prettyFeatureSet | Ide.Plugin.Tactic.FeatureSet |
| Provenance | Ide.Plugin.Tactic.Types |
| pushRecursionStack | Ide.Plugin.Tactic.Types |
| pv_ancestry | Ide.Plugin.Tactic.Types |
| pv_datacon | Ide.Plugin.Tactic.Types |
| pv_position | Ide.Plugin.Tactic.Types |
| pv_scrutinee | Ide.Plugin.Tactic.Types |
| Range | Ide.Plugin.Tactic.Types |
| rangeToRealSrcSpan | Ide.Plugin.Tactic.Range |
| rangeToSrcSpan | Ide.Plugin.Tactic.Range |
| recursion | Ide.Plugin.Tactic.Tactics |
| RecursionOnWrongParam | Ide.Plugin.Tactic.Types |
| RecursiveCall | Ide.Plugin.Tactic.Types |
| RecursivePrv | Ide.Plugin.Tactic.Types |
| requireConcreteHole | Ide.Plugin.Tactic.Machinery |
| requireNewHoles | Ide.Plugin.Tactic.Tactics |
| Reward | |
| 1 (Type/Class) | Ide.Plugin.Tactic.Machinery |
| 2 (Data Constructor) | Ide.Plugin.Tactic.Machinery |
| Rose | |
| 1 (Type/Class) | Ide.Plugin.Tactic.Types |
| 2 (Data Constructor) | Ide.Plugin.Tactic.Types |
| rose | Ide.Plugin.Tactic.Types |
| rtr_ctx | Ide.Plugin.Tactic.Types |
| rtr_extract | Ide.Plugin.Tactic.Types |
| rtr_jdg | Ide.Plugin.Tactic.Types |
| rtr_other_solns | Ide.Plugin.Tactic.Types |
| rtr_trace | Ide.Plugin.Tactic.Types |
| Rule | Ide.Plugin.Tactic.Types |
| RuleM | Ide.Plugin.Tactic.Types |
| runIde | Ide.Plugin.Tactic.LanguageServer |
| runStaleIde | Ide.Plugin.Tactic.LanguageServer |
| runTactic | Ide.Plugin.Tactic.Machinery, Ide.Plugin.Tactic.Tactics |
| RunTacticResults | |
| 1 (Type/Class) | Ide.Plugin.Tactic.Types |
| 2 (Data Constructor) | Ide.Plugin.Tactic.Types |
| scoreSolution | Ide.Plugin.Tactic.Machinery |
| Shadowed | Ide.Plugin.Tactic.Types |
| simplify | Ide.Plugin.Tactic.Simplify |
| SinglePatMatch | Ide.Plugin.Tactic.GHC |
| solutionSize | Ide.Plugin.Tactic.Machinery |
| Span | Ide.Plugin.Tactic.Types |
| spliceProvenance | Ide.Plugin.Tactic.LanguageServer |
| split | Ide.Plugin.Tactic.Tactics |
| splitAuto | Ide.Plugin.Tactic.Tactics |
| splitDataCon | Ide.Plugin.Tactic.Tactics |
| splitId | Ide.Plugin.Tactic.Context |
| splitToDecl | Ide.Plugin.Tactic.CaseSplit |
| substCTy | Ide.Plugin.Tactic.Machinery |
| substJdg | Ide.Plugin.Tactic.Judgements |
| TacticCommand | Ide.Plugin.Tactic.TestTypes, Ide.Plugin.Tactic |
| tacticDesc | Ide.Plugin.Tactic.LanguageServer |
| TacticError | Ide.Plugin.Tactic.Types |
| TacticParams | |
| 1 (Type/Class) | Ide.Plugin.Tactic.LanguageServer.TacticProviders |
| 2 (Data Constructor) | Ide.Plugin.Tactic.LanguageServer.TacticProviders |
| TacticsM | Ide.Plugin.Tactic.Types |
| tacticsSplitFunTy | Ide.Plugin.Tactic.GHC |
| TacticState | |
| 1 (Type/Class) | Ide.Plugin.Tactic.Types |
| 2 (Data Constructor) | Ide.Plugin.Tactic.Types |
| tacticsThetaTy | Ide.Plugin.Tactic.GHC |
| tacticTitle | Ide.Plugin.Tactic.TestTypes, Ide.Plugin.Tactic |
| tcCommandId | Ide.Plugin.Tactic.LanguageServer.TacticProviders |
| tcCommandName | Ide.Plugin.Tactic.LanguageServer |
| tcTyVar_maybe | Ide.Plugin.Tactic.GHC |
| TooPolymorphic | Ide.Plugin.Tactic.Types |
| TopLevelArgPrv | Ide.Plugin.Tactic.Types |
| TopLevelRHS | Ide.Plugin.Tactic.GHC |
| tp_file | Ide.Plugin.Tactic.LanguageServer.TacticProviders |
| tp_range | Ide.Plugin.Tactic.LanguageServer.TacticProviders |
| tp_var_name | Ide.Plugin.Tactic.LanguageServer.TacticProviders |
| Trace | Ide.Plugin.Tactic.Types |
| trace | Ide.Plugin.Tactic.Debug, Ide.Plugin.Tactic.Types |
| traceFX | Ide.Plugin.Tactic.Debug, Ide.Plugin.Tactic.Types |
| traceIdX | Ide.Plugin.Tactic.Debug, Ide.Plugin.Tactic.Types |
| traceM | Ide.Plugin.Tactic.Debug, Ide.Plugin.Tactic.Types |
| traceMX | Ide.Plugin.Tactic.Debug, Ide.Plugin.Tactic.Types |
| tracePrim | Ide.Plugin.Tactic.Machinery |
| traceShowId | Ide.Plugin.Tactic.Debug, Ide.Plugin.Tactic.Types |
| traceX | Ide.Plugin.Tactic.Debug, Ide.Plugin.Tactic.Types |
| tracing | Ide.Plugin.Tactic.Machinery |
| tryUnifyUnivarsButNotSkolems | Ide.Plugin.Tactic.Machinery |
| ts_intro_vals | Ide.Plugin.Tactic.Types |
| ts_recursion_count | Ide.Plugin.Tactic.Types |
| ts_recursion_stack | Ide.Plugin.Tactic.Types |
| ts_skolems | Ide.Plugin.Tactic.Types |
| ts_unifier | Ide.Plugin.Tactic.Types |
| ts_unique_gen | Ide.Plugin.Tactic.Types |
| ts_unused_top_vals | Ide.Plugin.Tactic.Types |
| ts_used_vals | Ide.Plugin.Tactic.Types |
| Type | Ide.Plugin.Tactic.Types |
| TyVar | Ide.Plugin.Tactic.Types |
| unCType | Ide.Plugin.Tactic.Types |
| UndefinedHypothesis | Ide.Plugin.Tactic.Types |
| unExtractM | Ide.Plugin.Tactic.Types |
| UnguardedRHSs | Ide.Plugin.Tactic.GHC |
| UnhelpfulDestruct | Ide.Plugin.Tactic.Types |
| UnhelpfulSplit | Ide.Plugin.Tactic.Types |
| unHypothesis | Ide.Plugin.Tactic.Types |
| UnificationError | Ide.Plugin.Tactic.Types |
| unify | Ide.Plugin.Tactic.Machinery |
| Uniquely | |
| 1 (Type/Class) | Ide.Plugin.Tactic.Types |
| 2 (Data Constructor) | Ide.Plugin.Tactic.Types |
| unpackMatches | Ide.Plugin.Tactic.GHC |
| unsafeDefaultUniqueSupply | Ide.Plugin.Tactic.Types |
| unsafeRender | Ide.Plugin.Tactic.Debug, Ide.Plugin.Tactic.Types |
| unsafeRender' | Ide.Plugin.Tactic.Debug, Ide.Plugin.Tactic.Types |
| unsetIsTopHole | Ide.Plugin.Tactic.Judgements |
| UnsolvedSubgoals | Ide.Plugin.Tactic.Types |
| unwhitelistingSplit | Ide.Plugin.Tactic.Judgements |
| unXPat | Ide.Plugin.Tactic.GHC |
| unzipTrace | Ide.Plugin.Tactic.CodeGen |
| useOccName | Ide.Plugin.Tactic.CodeGen |
| UserPrv | Ide.Plugin.Tactic.Types |
| var' | Ide.Plugin.Tactic.CodeGen.Utils, Ide.Plugin.Tactic.CodeGen |
| withIntroducedVals | Ide.Plugin.Tactic.Types |
| withNewGoal | Ide.Plugin.Tactic.Judgements |
| withRecursionStack | Ide.Plugin.Tactic.Types |
| withUsedVals | Ide.Plugin.Tactic.Types |
| WrongBranch | Ide.Plugin.Tactic.Types |
| _jBlacklistDestruct | Ide.Plugin.Tactic.Types |
| _jGoal | Ide.Plugin.Tactic.Types |
| _jHypothesis | Ide.Plugin.Tactic.Types |
| _jIsTopHole | Ide.Plugin.Tactic.Types |
| _jWhitelistSplit | Ide.Plugin.Tactic.Types |