Skip to content

Commit

Permalink
Added the note Alex suggested
Browse files Browse the repository at this point in the history
  • Loading branch information
LuqiPan committed Apr 20, 2015
1 parent 78f17ef commit 2d76f75
Showing 1 changed file with 2 additions and 1 deletion.
3 changes: 2 additions & 1 deletion idris/tutorial.md
Original file line number Diff line number Diff line change
Expand Up @@ -467,7 +467,8 @@ namespace vect
The first thing to note is that, in order to not clash names with our list
constructors, we'll have to put all our vector-related code in a namespace.
The following functions should all be indented and put in this namespace.
(Alternatively, you can just put this code in a separate file.)
(Alternatively, you can just put this code in a separate file.
**NOTE**: Don't forget to include the line `infixr 5 ::`)

Unlike our `List` type before, our `Vector` type has an extra parameter which
is it's length. So `Vector (S (S Z)) Integer` is the type of list of three
Expand Down

0 comments on commit 2d76f75

Please sign in to comment.