Index

.+	Cornelis.Offsets
.-.	Cornelis.Offsets
AbsolutePath
1 (Type/Class)	Cornelis.Types.Agda
2 (Data Constructor)	Cornelis.Types.Agda
addCol	Cornelis.Offsets
addHighlight	Cornelis.Highlighting
Agda
1 (Type/Class)	Cornelis.Types
2 (Data Constructor)	Cornelis.Types
AgdaIndex	Cornelis.Offsets
AgdaInterval	Cornelis.Offsets
AgdaOffset	Cornelis.Offsets
AgdaPos
1 (Type/Class)	Cornelis.Offsets
2 (Data Constructor)	Cornelis.Types
AgdaPos'	Cornelis.Types
AgdaResp
1 (Type/Class)	Cornelis.Types
2 (Data Constructor)	Cornelis.Types
allGoals	Plugin
AllGoalsWarnings	Cornelis.Types
applyOver	Cornelis.Subscripts
ar_buffer	Cornelis.Types
ar_message	Cornelis.Types
AsIs	Cornelis.Types.Agda
atomicSwapIORef	Plugin
atomToHlGroup	Cornelis.Pretty
autoOne	Plugin
a_buffer	Cornelis.Types
a_hdl	Cornelis.Types
a_ready	Cornelis.Types
a_req	Cornelis.Types
Backward	Cornelis.Vim
bs_agda_proc	Cornelis.Types
bs_code_map	Cornelis.Types
bs_goals	Cornelis.Types
bs_goto_sites	Cornelis.Types
bs_info_win	Cornelis.Types
bs_ips	Cornelis.Types
bs_ip_exts	Cornelis.Types
Buffer	Cornelis.Types
BufferNum	Cornelis.Types
BufferStuff
1 (Type/Class)	Cornelis.Types
2 (Data Constructor)	Cornelis.Types
buildInfoBuffer	Cornelis.InfoWin
buildIOTCM	Cornelis.Agda
Byte	Cornelis.Offsets
caseSplit	Plugin
cc_max_height	Cornelis.Types
cc_max_width	Cornelis.Types
cc_split_location	Cornelis.Types
ce_config	Cornelis.Types
ce_namespace	Cornelis.Types
ce_state	Cornelis.Types
ce_stream	Cornelis.Types
charToBytes	Cornelis.Offsets
ClearHighlighting	Cornelis.Types
ClearRunningInfo	Cornelis.Types
closeInfoWindows	Cornelis.InfoWin
Cmd_abort	Cornelis.Types.Agda
Cmd_autoAll	Cornelis.Types.Agda
Cmd_autoOne	Cornelis.Types.Agda
Cmd_compute	Cornelis.Types.Agda
Cmd_compute_toplevel	Cornelis.Types.Agda
Cmd_constraints	Cornelis.Types.Agda
Cmd_context	Cornelis.Types.Agda
Cmd_elaborate_give	Cornelis.Types.Agda
Cmd_exit	Cornelis.Types.Agda
Cmd_give	Cornelis.Types.Agda
Cmd_goal_type	Cornelis.Types.Agda
Cmd_goal_type_context	Cornelis.Types.Agda
Cmd_goal_type_context_check	Cornelis.Types.Agda
Cmd_goal_type_context_infer	Cornelis.Types.Agda
Cmd_helper_function	Cornelis.Types.Agda
Cmd_highlight	Cornelis.Types.Agda
Cmd_infer	Cornelis.Types.Agda
Cmd_infer_toplevel	Cornelis.Types.Agda
Cmd_intro	Cornelis.Types.Agda
Cmd_load	Cornelis.Types.Agda
Cmd_load_highlighting_info	Cornelis.Types.Agda
Cmd_make_case	Cornelis.Types.Agda
Cmd_metas	Cornelis.Types.Agda
Cmd_refine	Cornelis.Types.Agda
Cmd_refine_or_intro	Cornelis.Types.Agda
Cmd_search_about_toplevel	Cornelis.Types.Agda
Cmd_show_module_contents	Cornelis.Types.Agda
Cmd_show_module_contents_toplevel	Cornelis.Types.Agda
Cmd_show_version	Cornelis.Types.Agda
Cmd_solveAll	Cornelis.Types.Agda
Cmd_solveOne	Cornelis.Types.Agda
Cmd_tokenHighlighting	Cornelis.Types.Agda
Cmd_why_in_scope	Cornelis.Types.Agda
Cmd_why_in_scope_toplevel	Cornelis.Types.Agda
CodePoint	Cornelis.Offsets
Colline
1 (Type/Class)	Cornelis.Diff
2 (Data Constructor)	Cornelis.Diff
Command
1 (Data Constructor)	Cornelis.Types.Agda
2 (Type/Class)	Cornelis.Types.Agda
Command'	Cornelis.Types.Agda
ComputeMode	Cornelis.Types.Agda
computeMode	Plugin
computeModeCompletion	Plugin
containsPoint	Cornelis.Offsets
cornelis	Lib
CornelisArgument	Cornelis.Pretty
CornelisBound	Cornelis.Pretty
CornelisCatchAllClause	Cornelis.Pretty
CornelisCoinductiveConstructor	Cornelis.Pretty
CornelisComment	Cornelis.Pretty
CornelisConfig
1 (Type/Class)	Cornelis.Types
2 (Data Constructor)	Cornelis.Types
CornelisEnv
1 (Type/Class)	Cornelis.Types
2 (Data Constructor)	Cornelis.Types
CornelisError	Cornelis.Pretty
CornelisErrorWarning	Cornelis.Pretty
CornelisField	Cornelis.Pretty
CornelisFunction	Cornelis.Pretty
CornelisGeneralizable	Cornelis.Pretty
CornelisHole	Cornelis.Pretty
CornelisInductiveConstructor	Cornelis.Pretty
cornelisInit	Lib
CornelisKeyword	Cornelis.Pretty
CornelisMacro	Cornelis.Pretty
CornelisModule	Cornelis.Pretty
CornelisName	Cornelis.Pretty
CornelisNumber	Cornelis.Pretty
CornelisOperator	Cornelis.Pretty
CornelisPostulate	Cornelis.Pretty
CornelisPragma	Cornelis.Pretty
CornelisPrimitive	Cornelis.Pretty
CornelisPrimitiveType	Cornelis.Pretty
CornelisRecord	Cornelis.Pretty
CornelisState
1 (Type/Class)	Cornelis.Types
2 (Data Constructor)	Cornelis.Types
CornelisString	Cornelis.Pretty
CornelisSymbol	Cornelis.Pretty
CornelisTitle	Cornelis.Pretty
CornelisType	Cornelis.Pretty
CornelisTypeChecks	Cornelis.Pretty
CornelisUnsolvedConstraint	Cornelis.Pretty
CornelisUnsolvedMeta	Cornelis.Pretty
CornelisWarn	Cornelis.Pretty
criticalFailure	Cornelis.Utils
cs_buffers	Cornelis.Types
cs_diff	Cornelis.Types
debug	Cornelis.Debug
DebugCommand	Cornelis.Types
debugCommandCompletion	Plugin
debugJson	Cornelis.Agda
decNextDigitSeq	Cornelis.Subscripts
DefaultCompute	Cornelis.Types.Agda
DefinitionSite
1 (Type/Class)	Cornelis.Types
2 (Data Constructor)	Cornelis.Types
Diff0	Cornelis.Types
Digits	Cornelis.Subscripts
digits	Cornelis.Subscripts
digitToInt	Cornelis.Subscripts
Direct	Cornelis.Types.Agda
DisplayError	Cornelis.Types
DisplayInfo
1 (Type/Class)	Cornelis.Types
2 (Data Constructor)	Cornelis.Types
di_all_invisible	Cornelis.Types
di_all_visible	Cornelis.Types
di_boundary	Cornelis.Types
di_errors	Cornelis.Types
di_in_scope	Cornelis.Types
di_ips	Cornelis.Types
di_output_forms	Cornelis.Types
di_type	Cornelis.Types
di_type_aux	Cornelis.Types
di_warnings	Cornelis.Types
doAbort	Plugin
doAllGoals	Plugin
doCaseSplit	Plugin
doCloseInfoWindows	Plugin
doDebug	Plugin
doDecNextDigitSeq	Lib
doElaborate	Plugin
doGive	Plugin
doGotoDefinition	Plugin
doHelperFunc	Plugin
doIncNextDigitSeq	Lib
doLoad	Plugin
doMakeCase	Lib
Done	Cornelis.Types.Agda
doNextGoal	Lib
doNormalize	Plugin
doPrevGoal	Lib
doQuestionToMeta	Plugin
doRefine	Plugin
doRestart	Plugin
doTypeInfer	Plugin
doWhyInScope	Plugin
DPos	Cornelis.Types
dropPrefix	Cornelis.Agda
ds_filepath	Cornelis.Types
ds_position	Cornelis.Types
DumpIPs	Cornelis.Types
elaborate	Plugin
Error	Cornelis.Types.Agda
es_hlgroup	Cornelis.Types
es_interval	Cornelis.Types
es_mark	Cornelis.Types
ExtendedLambda	Cornelis.Types
Extmark
1 (Type/Class)	Cornelis.Types
2 (Data Constructor)	Cornelis.Types
ExtmarkStuff
1 (Type/Class)	Cornelis.Types
2 (Data Constructor)	Cornelis.Types
extract	Cornelis.Subscripts
findGoal	Cornelis.Goals
Flavor	Cornelis.Subscripts
Forward	Cornelis.Vim
fromBytes	Cornelis.Offsets
fromOneIndexed	Cornelis.Offsets
fromZeroIndexed	Cornelis.Offsets
Function	Cornelis.Types
getAgda	Cornelis.Agda
getBufferInterval	Cornelis.Vim
getBufferLine	Cornelis.Vim
getConfig	Cornelis.Config
getDefinitionSites	Plugin
getExtmarkIntervalById	Cornelis.Vim
getExtmarks	Cornelis.Highlighting
getGoalAtCursor	Cornelis.Goals
getGoalAtPos	Cornelis.Goals
getGoalContents	Cornelis.Goals
getGoalContentsMaybe	Cornelis.Goals
getIndent	Cornelis.Vim
getInteractionPoint	Lib
getIpInterval	Cornelis.Goals
getLambdaClause	Cornelis.Vim
getLineIntervals	Cornelis.Highlighting
getMessage	Cornelis.Types
getpos	Cornelis.Vim
getSurroundingMotion	Cornelis.Vim
getVar	Cornelis.Config
getVarWithAlternatives	Cornelis.Config
getWindowCursor	Cornelis.Vim
give	Plugin
GiveAction	Cornelis.Types
gi_ip	Cornelis.Types
gi_type	Cornelis.Types
GoalInfo
1 (Type/Class)	Cornelis.Types
2 (Data Constructor)	Cornelis.Types
GoalSpecific	Cornelis.Types
goalWindow	Plugin
gotoDefinition	Plugin
groupScopeSet	Cornelis.Pretty
HasCallStack	Cornelis.Types
HeadCompute	Cornelis.Types.Agda
HeadNormal	Cornelis.Types.Agda
helperFunc	Plugin
HelperFunction	Cornelis.Types
Highlight
1 (Type/Class)	Cornelis.Types
2 (Data Constructor)	Cornelis.Types
highlightBuffer	Cornelis.Highlighting
HighlightGroup	Cornelis.Pretty
HighlightingInfo	Cornelis.Types
HighlightingLevel	Cornelis.Types.Agda
HighlightingMethod	Cornelis.Types.Agda
highlightInterval	Cornelis.Highlighting
hl_atoms	Cornelis.Types
hl_definitionSite	Cornelis.Types
hl_end	Cornelis.Types
hl_start	Cornelis.Types
Horizontal	Cornelis.Types
iEnd	Cornelis.Offsets
IgnoreAbstract	Cornelis.Types.Agda
ihl_end	Cornelis.Pretty
ihl_group	Cornelis.Pretty
ihl_start	Cornelis.Pretty
incIndex	Cornelis.Offsets
incNextDigitSeq	Cornelis.Subscripts
indent	Lib
Index	Cornelis.Offsets
Indexing	Cornelis.Offsets
Indirect	Cornelis.Types.Agda
InferredType	Cornelis.Types
inferType	Plugin
InfoBuffer
1 (Type/Class)	Cornelis.Types
2 (Data Constructor)	Cornelis.Types
InfoHighlight
1 (Type/Class)	Cornelis.Pretty
2 (Data Constructor)	Cornelis.Pretty
InScope
1 (Type/Class)	Cornelis.Types
2 (Data Constructor)	Cornelis.Types
Instantiated	Cornelis.Types.Agda
Interaction	Cornelis.Types.Agda
Interaction'	Cornelis.Types.Agda
InteractionId
1 (Type/Class)	Cornelis.Types.Agda, Cornelis.Types
2 (Data Constructor)	Cornelis.Types.Agda
interactionId	Cornelis.Types.Agda
InteractionPoint
1 (Type/Class)	Cornelis.Types
2 (Data Constructor)	Cornelis.Types
InteractionPoints	Cornelis.Types
Interactive	Cornelis.Types.Agda
Interval
1 (Type/Class)	Cornelis.Offsets
2 (Data Constructor)	Cornelis.Offsets
intervalsToRange	Cornelis.Types.Agda
intervalToRange	Cornelis.Types.Agda
IntervalWithoutFile	Cornelis.Types.Agda
IOTCM
1 (Data Constructor)	Cornelis.Types.Agda
2 (Type/Class)	Cornelis.Types.Agda
IOTCM'	Cornelis.Types.Agda
ip_id	Cornelis.Types
ip_interval'	Cornelis.Types
ip_intervalM	Cornelis.Types
isEmpty	Cornelis.Pretty
iStart	Cornelis.Offsets
is_in_scope	Cornelis.Types
is_original_name	Cornelis.Types
is_refied_name	Cornelis.Types
is_type	Cornelis.Types
iw_buffer	Cornelis.Types
JumpToError	Cornelis.Types
Keep	Cornelis.Types.Agda
Line	Cornelis.Offsets
LineIntervals
1 (Type/Class)	Cornelis.Types
2 (Data Constructor)	Cornelis.Types
lineIntervalsForBuffer	Cornelis.Highlighting
LineNumber	Cornelis.Offsets
li_intervalMap	Cornelis.Types
load	Plugin
lookupPoint	Cornelis.Highlighting
main	Lib
MakeCase
1 (Type/Class)	Cornelis.Types
2 (Data Constructor)	Cornelis.Types
MakeCaseVariant	Cornelis.Types
Message
1 (Type/Class)	Cornelis.Types
2 (Data Constructor)	Cornelis.Types
mkAbsPathRnage	Cornelis.Types.Agda
mkReplacement	Cornelis.Subscripts
modifyBufferStuff	Cornelis.Utils
NamedPoint
1 (Type/Class)	Cornelis.Types
2 (Data Constructor)	Cornelis.Types
neovimAsync	Cornelis.Utils
nextGoal	Cornelis.Goals
None	Cornelis.Types.Agda
NonInteractive	Cornelis.Types.Agda
NoRange	Cornelis.Types.Agda
noRange	Cornelis.Types.Agda
NormalForm	Cornelis.Types
Normalised	Cornelis.Types.Agda
normalizationMode	Plugin
notifyEdit	Plugin
np_interval	Cornelis.Types
np_name	Cornelis.Types
objectToInt	Cornelis.Utils
objectToText	Cornelis.Utils
Offset
1 (Type/Class)	Cornelis.Offsets
2 (Data Constructor)	Cornelis.Offsets
offsetPlus	Cornelis.Offsets
OnBottom	Cornelis.Types
oneIndex	Cornelis.Offsets
OneIndexed	Cornelis.Offsets
OnLeft	Cornelis.Types
OnRight	Cornelis.Types
OnTop	Cornelis.Types
overNextDigitSeq	Cornelis.Subscripts
parseDigits	Cornelis.Subscripts
parseExtmark	Cornelis.Highlighting
parseFlavor	Cornelis.Subscripts
parseLine	Cornelis.Subscripts
parseNum	Cornelis.Subscripts
Parser	Cornelis.Subscripts
Pos
1 (Type/Class)	Cornelis.Offsets
2 (Data Constructor)	Cornelis.Offsets
prettyError	Cornelis.Pretty
prettyGoal	Cornelis.Pretty
prettyGoals	Cornelis.Pretty
prettyInScope	Cornelis.Pretty
prettyInScopeSet	Cornelis.Pretty
prettyInterval	Cornelis.Pretty
prettyManyGoals	Cornelis.Pretty
prettyName	Cornelis.Pretty
prettyPoint	Cornelis.Pretty
prettyType	Cornelis.Pretty
prettyVisibleName	Cornelis.Pretty
prevGoal	Cornelis.Goals
priority	Cornelis.Pretty
p_col	Cornelis.Offsets
p_line	Cornelis.Offsets
questionToMeta	Plugin
Range
1 (Type/Class)	Cornelis.Types.Agda
2 (Data Constructor)	Cornelis.Types.Agda
Range'	Cornelis.Types.Agda
readSplitLocation	Cornelis.Types
recordUpdate	Cornelis.Diff
refine	Plugin
RegularCase	Cornelis.Types
Remove
1 (Type/Class)	Cornelis.Types.Agda
2 (Data Constructor)	Cornelis.Types.Agda
renderWithHlGroups	Cornelis.Pretty
Replace
1 (Type/Class)	Cornelis.Diff
2 (Data Constructor)	Cornelis.Diff
replace	Cornelis.Subscripts
replaceInterval	Cornelis.Vim
replaceQuestion	Cornelis.Goals
reportError	Cornelis.Vim
reportExceptions	Cornelis.Debug
reportInfo	Cornelis.Vim
resetDiff	Cornelis.Diff
respond	Lib
respondToHelperFunction	Lib
Response	Cornelis.Types
Rewrite	Cornelis.Types.Agda
rewriteModeCompletion	Plugin
runInteraction	Plugin
runIOTCM	Cornelis.Agda
RunningInfo	Cornelis.Types
savingCurrentPosition	Cornelis.Utils
savingCurrentWindow	Cornelis.Utils
SearchMode	Cornelis.Vim
searchpos	Cornelis.Vim
section	Cornelis.Pretty
sequenceInteractionPoint	Cornelis.Types
setHighlight	Cornelis.Highlighting
setHighlight'	Cornelis.Highlighting
setreg	Cornelis.Vim
setWindowCursor	Cornelis.Vim
ShowImplicitArgs	Cornelis.Types.Agda
showInfoWindow	Cornelis.InfoWin
ShowIrrelevantArgs	Cornelis.Types.Agda
Simplified	Cornelis.Types.Agda
Solution
1 (Type/Class)	Cornelis.Types
2 (Data Constructor)	Cornelis.Types
SolveAll	Cornelis.Types
solveOne	Plugin
spanInfoHighlights	Cornelis.Pretty
spawnAgda	Cornelis.Agda
SplitLocation	Cornelis.Types
SrcFile	Cornelis.Types.Agda
Status	Cornelis.Types
status_checked	Cornelis.Types
status_showImplicits	Cornelis.Types
status_showIrrelevant	Cornelis.Types
Subscript	Cornelis.Subscripts
subscripts	Cornelis.Subscripts
Superscript	Cornelis.Subscripts
superscripts	Cornelis.Subscripts
s_expression	Cornelis.Types
s_ip	Cornelis.Types
ta_expr	Cornelis.Types
Text	Cornelis.Types
textPath	Cornelis.Types.Agda
textToBytes	Cornelis.Offsets
toBytes	Cornelis.Offsets
ToggleImplicitArgs	Cornelis.Types.Agda
ToggleIrrelevantArgs	Cornelis.Types.Agda
toOneIndexed	Cornelis.Offsets
toZeroIndexed	Cornelis.Offsets
traceMX	Cornelis.Debug, Cornelis.Types
translateInterval	Cornelis.Diff
Type
1 (Type/Class)	Cornelis.Types
2 (Data Constructor)	Cornelis.Types
TypeAux
1 (Type/Class)	Cornelis.Types
2 (Data Constructor)	Cornelis.Types
typeContext	Plugin
typeContextInfer	Plugin
Unit	Cornelis.Offsets
Unknown	Cornelis.Types
UnknownDisplayInfo	Cornelis.Types
unparse	Cornelis.Subscripts
unparseWith	Cornelis.Subscripts
unvimify	Cornelis.Vim
updateLineIntervals	Cornelis.Highlighting
UseForce	Cornelis.Types.Agda
UseShowInstance	Cornelis.Types.Agda
Vallee
1 (Type/Class)	Cornelis.Diff
2 (Data Constructor)	Cornelis.Diff
Vertical	Cornelis.Types
vimFirstLine	Cornelis.Vim
vimify	Cornelis.Vim
VimIndex	Cornelis.Offsets
VimInterval	Cornelis.Offsets
vimLastLine	Cornelis.Vim
VimOffset	Cornelis.Offsets
VimPos	Cornelis.Offsets
visibleBuffers	Cornelis.Utils
WhyInScope	Cornelis.Types
whyInScope	Plugin
Window	Cornelis.Types
windowsForBuffer	Cornelis.Utils
withAgda	Cornelis.Agda
withBufferStuff	Cornelis.Utils
withComputeMode	Plugin
withCurrentBuffer	Cornelis.Agda
WithForce	Cornelis.Types.Agda
withGoalAtCursor	Cornelis.Goals
withGoalContentsOrPrompt	Cornelis.Goals
withLocalEnv	Cornelis.Utils
withNormalizationMode	Plugin
WithoutForce	Cornelis.Types.Agda
zeroIndex	Cornelis.Offsets
ZeroIndexed	Cornelis.Offsets