Skip to content

Commit 0dd887f

Browse files
committed
Update documentation
1 parent d238beb commit 0dd887f

File tree

5 files changed

+16
-32
lines changed

5 files changed

+16
-32
lines changed

FEATURES.md

Lines changed: 13 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -1,91 +1,65 @@
11
### Typechecking
22

3-
`(shift + cmd/ctrl + t)`
4-
53
![typechecking](./images/screenshots/typechecking.gif)
64

75
### Showing the type of an identifier
86

9-
`(shift + cmd/ctrl + o)`
10-
117
![typeof](./images/screenshots/typeof.gif)
128

139
### Showing the docs for an identifier
1410

15-
`(shift + cmd/ctrl + d)`
16-
1711
![docsfor](./images/screenshots/docsfor.gif)
1812

1913
### Showing the definition for an identifier
2014

21-
`(shift + cmd/ctrl + f)`
22-
2315
![definition](./images/screenshots/definition.gif)
2416

2517
### List all the currently active holes
2618

27-
`(shift + cmd/ctrl + h)`
28-
2919
![showholes](./images/screenshots/showholes.gif)
3020

3121
### Generate an initial pattern match clause
3222

33-
`(shift + cmd/ctrl + a)`
34-
3523
![addclause](./images/screenshots/addclause.gif)
3624

37-
### Generate a case split for the pattern variable
25+
### Generate an initial pattern match clause when trying to proof a type
26+
27+
![addproofclause](./images/screenshots/addproofclause.gif)
3828

39-
`(shift + cmd/ctrl + c)`
29+
### Generate a case split for the pattern variable
4030

4131
![casesplit](./images/screenshots/casesplit.gif)
4232

4333
### Attempt to fill out the holes by proof search
4434

45-
`(shift + cmd/ctrl + s)`
46-
4735
![proofsearch](./images/screenshots/proofsearch.gif)
4836

4937
### Create a with rule pattern match template for the clause of function
5038

51-
`(shift + cmd/ctrl + w)`
52-
5339
![makewith](./images/screenshots/makewith.gif)
5440

5541
### Create a case pattern match template for the holes
5642

57-
`(shift + cmd/ctrl + m)`
58-
5943
![makecase](./images/screenshots/makecase.gif)
6044

6145
### Create a top level function with a type which solves the hole under the cursor
6246

63-
`(shift + cmd/ctrl + l)`
64-
6547
![makelemma](./images/screenshots/makelemma.gif)
6648

6749
### Search names, types and documentations
6850

69-
`(shift + cmd/ctrl + k)`
70-
7151
![apropos](./images/screenshots/apropos.gif)
7252

7353
### Evaluate selected code in editor
7454

75-
`(shift + cmd/ctrl + e)`
76-
7755
![eval-selection](./images/screenshots/eval-selection.gif)
7856

7957
### Start or Refresh REPL
8058

81-
`(shift + cmd/ctrl + r)`
82-
8359
![start-refresh-repl](./images/screenshots/start-refresh-repl.gif)
8460

8561
### Send selected code to REPL
8662

87-
`(shift + cmd/ctrl + x)`
88-
8963
![send-selection-repl](./images/screenshots/send-selection-repl.gif)
9064

9165
### ipkg highlighting
@@ -126,4 +100,12 @@
126100

127101
### Latex snippets
128102

129-
![latex-snippets](./images/screenshots/latex.gif)
103+
![latex-snippets](./images/screenshots/latex.gif)
104+
105+
### Literate Idris
106+
107+
![literate-idris](./images/screenshots/literate.gif)
108+
109+
### Type checking on saving file
110+
111+
![typechecing-on-save](./images/screenshots/typecheckingonsave.gif)

README.md

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@
1717
| [Show the doc for a definition](https://github.com/zjhmale/vscode-idris/blob/master/FEATURES.md#showing-the-definition-for-an-identifier) | idris.print-definition |
1818
| [Show holes](https://github.com/zjhmale/vscode-idris/blob/master/FEATURES.md#list-all-the-currently-active-holes) | idris.show-holes |
1919
| [Add clause](https://github.com/zjhmale/vscode-idris/blob/master/FEATURES.md#generate-an-initial-pattern-match-clause) | idris.add-clause |
20+
| [Add proof clause](https://github.com/zjhmale/vscode-idris/blob/master/FEATURES.md#generate-an-initial-pattern-match-clause-when-trying-to-proof-a-type) | idris.add-proof-clause |
2021
| [Split case](https://github.com/zjhmale/vscode-idris/blob/master/FEATURES.md#generate-a-case-split-for-the-pattern-variable) | idris.case-split |
2122
| [Search proof](https://github.com/zjhmale/vscode-idris/blob/master/FEATURES.md#attempt-to-fill-out-the-holes-by-proof-search) | idris.proof-search |
2223
| [Make with](https://github.com/zjhmale/vscode-idris/blob/master/FEATURES.md#create-a-with-rule-pattern-match-template-for-the-clause-of-function) | idris.make-with |
@@ -35,13 +36,14 @@
3536
* [ipkg highlighting](https://github.com/zjhmale/vscode-idris/blob/master/FEATURES.md#ipkg-highlighting)
3637
* [Auto-completion](https://github.com/zjhmale/vscode-idris/blob/master/FEATURES.md#code-completion)
3738
* [Show type definition on hover](https://github.com/zjhmale/vscode-idris/blob/master/FEATURES.md#show-type-definition-on-hover)
38-
* Type checking on saving file
39+
* [Type checking on saving file](https://github.com/zjhmale/vscode-idris/blob/master/FEATURES.md#type-checking-on-saving-file)
3940
* [Go to Definition and Peek Definition](https://github.com/zjhmale/vscode-idris/blob/master/FEATURES.md#go-to-definition-and-peek-definition)
4041
* [Go to Symbol (Outline symbols in currently opend file)](https://github.com/zjhmale/vscode-idris/blob/master/FEATURES.md#go-to-symbol-outline-symbols-in-currently-opend-file)
4142
* [Search Symbol (Outline symbols in currently opend project)](https://github.com/zjhmale/vscode-idris/blob/master/FEATURES.md#search-symbol-outline-symbols-in-currently-opend-project)
4243
* [Find all references](https://github.com/zjhmale/vscode-idris/blob/master/FEATURES.md#find-all-references)
4344
* [Rename symbol](https://github.com/zjhmale/vscode-idris/blob/master/FEATURES.md#rename-symbol)
4445
* [Latex snippets](https://github.com/zjhmale/vscode-idris/blob/master/FEATURES.md#latex-snippets)
46+
* [Literate Idris](https://github.com/zjhmale/vscode-idris/blob/master/FEATURES.md#literate-idris)
4547

4648
## Installation
4749

1.85 MB
Loading

images/screenshots/literate.gif

2.57 MB
Loading
2.84 MB
Loading

0 commit comments

Comments
 (0)