From f650b940d2c0f833ecbb6571ebee10ead433132b Mon Sep 17 00:00:00 2001 From: Brendan Zabarauskas Date: Sun, 13 Sep 2015 12:33:10 +1000 Subject: [PATCH 1/3] Fix code example --- documentation/tutorial.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/documentation/tutorial.md b/documentation/tutorial.md index a6a2ffe..2b015cb 100644 --- a/documentation/tutorial.md +++ b/documentation/tutorial.md @@ -145,7 +145,7 @@ plusAssoc (S l) c r = ?plusAssoc_rhs_2 with ```idris -plusAssoc (S l) c r = rewrite plusAssoc l r c in ?plusAssoc_rhs_2 +plusAssoc (S l) c r = rewrite plusAssoc l c r in ?plusAssoc_rhs_2 ``` and after type checking the holes view now shows us: From 2c085b0254e4b680c3120b75456045e4a124de03 Mon Sep 17 00:00:00 2001 From: Brendan Zabarauskas Date: Sun, 13 Sep 2015 12:34:09 +1000 Subject: [PATCH 2/3] Fix incorrect key binding --- documentation/tutorial.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/documentation/tutorial.md b/documentation/tutorial.md index 2b015cb..07cedc4 100644 --- a/documentation/tutorial.md +++ b/documentation/tutorial.md @@ -59,7 +59,7 @@ module Main plusAssoc : (l, c, r : Nat) -> l `plus` (c `plus` r) = (l `plus` c) `plus` r ``` -Load the file into idris by typecheckiing it by pressing `ctrl-shift-r`. Then press `ctrl-shift-p` and type "Language Idris: Holes". +Load the file into Idris by typechecking it by pressing `ctrl-alt-r`. Then press `ctrl-shift-p` and type "Language Idris: Holes". At the bottom of your window should open a small panel with all holes you'll have to prove. Here it should just show: From b11d7f5ff0b59157cf4b5495b25f250496fa638e Mon Sep 17 00:00:00 2001 From: Brendan Zabarauskas Date: Sun, 13 Sep 2015 12:35:03 +1000 Subject: [PATCH 3/3] Formatting, spelling, and grammar fixes --- documentation/tutorial.md | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/documentation/tutorial.md b/documentation/tutorial.md index 07cedc4..516a7b3 100644 --- a/documentation/tutorial.md +++ b/documentation/tutorial.md @@ -4,8 +4,7 @@ ## Learning Idris -This is an overview over the atom package for Idris. -If you are interested in learning Idris you can find the official documentation here http://docs.idris-lang.org/en/latest/ and the official Idris tutorial here http://eb.host.cs.st-andrews.ac.uk/writings/idris-tutorial.pdf. +This is an overview of the atom package for Idris. If you are interested in learning Idris you can find the [official documentation](http://docs.idris-lang.org/en/latest/), and the [official Idris tutorial](http://docs.idris-lang.org/en/latest/tutorial/). ### Installation @@ -36,8 +35,7 @@ Open the command palette (`ctrl-shift-p` on Win/Linux) and select `Language Idri ### Type info -Select an instance of the `add` function in your code and press `ctrl-alt-t` or use the command palette (`ctrl-shift-p` on Win/Linux) and search for "Language Idris: Type Of". -A panel should open at the bottom of your window showing you the type of the `add` function, `Ops.add : Nat -> Nat -> Nat`. +Select an instance of the `add` function in your code and press `ctrl-alt-t` or use the command palette (`ctrl-shift-p` on Win/Linux) and search for "Language Idris: Type Of". A panel should open at the bottom of your window showing you the type of the `add` function, `Ops.add : Nat -> Nat -> Nat`. Now try the same thing with the `mul` function. ### Show documentation @@ -160,7 +158,7 @@ Main.plusAssoc_rhs_2 Main.plusAssoc_rhs_2 : S (plus (plus l c) r) = S (plus (plus l c) r) ``` -Now you need to prove that `S (plus (plus l c) r) = S (plus (plus l c) r)` and Idrs can again do this for us. +Now you need to prove that `S (plus (plus l c) r) = S (plus (plus l c) r)` and Idris can again do this for us. And you end with the file @@ -174,5 +172,5 @@ plusAssoc (S l) c r = rewrite plusAssoc l c r in Refl and a proof that the addition of natural numbers is associative. -This tutorial is a written version of [David Christiansens](https://twitter.com/d_christiansen) emacs video for Atom. +This tutorial is a written version of [David Christiansen's](https://twitter.com/d_christiansen) emacs video for Atom. https://www.youtube.com/watch?v=0eOY1NxbZHo&list=PLiHLLF-foEexGJu1a0WH_llkQ2gOKqipg