-
Notifications
You must be signed in to change notification settings - Fork 26
/
idris2-vim.txt
154 lines (111 loc) · 6.88 KB
/
idris2-vim.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
*idris2-vim.txt* Last change 2020 February 22
===============================================================================
===============================================================================
@@@@ @@@@@@@@ @@@@@@@@ @@@@ @@@@@@ @@ @@ @@@@ @@ @@
@@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@@ @@@
@@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@@@ @@@@
@@ @@ @@ @@@@@@@@ @@ @@@@@@ @@@@@@@ @@ @@ @@ @@ @@@ @@
@@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@
@@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@ @@
@@@@ @@@@@@@@ @@ @@ @@@@ @@@@@@ @@@ @@@@ @@ @@
===============================================================================
CONTENTS *idris-vim-contents*
1. Features: |idris-vim-features|
2. Requirements: |idris-vim-requirements|
3. Functions: |idris-vim-functions|
4. Troubleshooting |idris-vim-troubleshooting|
5. Examples: |idris-vim-examples|
6. Information: |idris-vim-information|
===============================================================================
FEATURES *idris-vim-features*
* Syntax Highlighting
* Indentation
* Unicode Concealing
* Syntax Checking (via Syntastic(https://github.com/scrooloose/syntastic))
* Interactive Editing via the REPL
===============================================================================
REQUIREMENTS *idris-vim-requirements*
* Idris2 (https://github.com/edwinb/Idris2/)
OPTIONAL:
* Syntastic(https://github.com/scrooloose/syntastic) for syntax checking
* Vimshell(https://github.com/Shougo/vimshell.vim) for a REPL
===============================================================================
FUNCTIONS *idris-vim-functions*
All of the functions in idris-vim are essentially just calls back to the REPL,
so documentation for each of them is also available there.
IdrisDocumentation *IdrisDocumentation*
Shows internal documentation of the primitive under the cursor.
Mapped to '<LocalLeader>_h' by default.
IdrisResponseWin *IdrisResponseWin*
This opens an idris response window in a new pane.
Mapped to '<LocalLeader>_i' by default.
IdrisShowType *IdrisShowType*
This shows the type of the name under the cursor (or, if the cursor happens
to be over a metavariable, a bit more information about its context).
Mapped to '<LocalLeader>_t' by default.
IdrisReload *IdrisReload*
This reloads the file and type-checks the file in the current buffer.
Mapped to '<LocalLeader>_r' by default.
IdrisEval *IdrisEval*
This prompts for an expression and then evaluates it in the REPL, then
returns the result.
Mapped to '<LocalLeader>_e' by default.
IdrisCaseSplit *IdrisCaseSplit*
When the cursor is over a variable in a pattern match clause or case
expression, this splits the variable into all well-typed patterns.
Mapped to '<LocalLeader>_c' by default
IdrisAddClause *IdrisAddClause*
When the cursor is at a type declaration this creates a new clause for that
signature.
By default mapped to '<LocalLeader>_d' for an ordinary top-level definition,
'<LocalLeader>_b' for a typeclass instance definition, and
'<LocalLeader>_md' to add a pattern-matching proof clause.
IdrisAddMissing: *IdrisAddMissing*
When the cursor is over a function, this adds all clauses necessary to make
that function cover all inputs. This also eliminates clauses which would
lead to unification errors from appearing.
Mapped to '<LocalLeader>_m' by default
IdrisRefine: *IdrisRefine*
Refines the item the cursor is over (applies the name and fills in any
arguments which can be filled in via unification)
Mapped to '<LocalLeader>_f' by default
IdrisProofSearch: *IdrisProofSearch*
This attempts to find a value for the metavariable it was called on by
looking at the rest of the code. It can also be called with hints, which
are functions that can apply to help solve for the metavariable.
Mapped to '<LocalLeader>_o' without hints and '<LocalLeader>p' with hints by
default
IdrisMakeWith: *IdrisMakeWith*
When the cursor is over a pattern clause and this is called, it creates a
new with clause.
Mapped to '<LocalLeader>_w' by default
IdrisMakeLemma: *IdrisMakeLemma*
When the cursor is over a metavariable and this is called, it creates a new
top-level definition to solve the metavariable.
Mapped to '<LocalLeader>_l' by default
===============================================================================
TROUBLESHOOTING *idris-vim-troubleshooting*
If this isn't working for you, make sure that:
* There is an Idris REPL running
* For syntax checking, you have syntastic installed
* The plugins mappings exists and don't conflict with anything else installed
(You can use ':map' to check. There should be mappings similar to
'\h * :call IdrisShowDoc()'.)
* Vim recognizes you're in an idris file (you can use ':verb set ft' to check)
If none of this works, check to issue tracker on github and if nothing is
there create an issue with a detailed description of the problem.
===============================================================================
EXAMPLES *idris-vim-examples*
Some excellent tutorials/examples for interactive editing using the above
functions can be found at:
http://edwinb.wordpress.com/2013/10/28/interactive-idris-editing-with-vim/
and
http://www.scribd.com/doc/214031954/60/Interactive-Editing-in-Vim
===============================================================================
INFORMATION *idris-vim-information*
Author: edwinb
Repo: https://github.com/idris-hackers/idris-vim
Documentation by japesinator
===============================================================================
===============================================================================
" vim:ft=help:et:ts=2:sw=2:sts=2:norl: