cornelis-0.2.0.0
Quick Jump
Contents
Index
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