|
2 | 2 |
|
3 | 3 | Welcome to my Idris 2 tutorial. I'll try and treat as many aspects |
4 | 4 | of the Idris 2 programming language as possible here. |
5 | | -All `.md` files in here a literate Idris files: They consist of |
| 5 | +All `.md` files in here are literate Idris files: They consist of |
6 | 6 | Markdown (hence the `.md` ending), which is being pretty printed |
7 | 7 | by GitHub together with Idris code blocks, which can be |
8 | 8 | type checked and built by the Idris compiler (more on this later). |
@@ -90,7 +90,7 @@ There are, of course, also some disadvantages: |
90 | 90 | ### Dependent Types |
91 | 91 |
|
92 | 92 | Idris is a strongly, statically typed programming language. This |
93 | | -means, that every Idris expression is given a *type* (for instance: |
| 93 | +means that every Idris expression is given a *type* (for instance: |
94 | 94 | integer, list of strings, boolean, function from integer to boolean, etc.) |
95 | 95 | and types are verified at compile time to rule out certain |
96 | 96 | common programming errors. |
@@ -270,7 +270,7 @@ maxBits8 = 255 |
270 | 270 |
|
271 | 271 | The first line can be read as: "We'd like to declare (nullary) |
272 | 272 | function `maxBits8`. It is of type `Bits8`". This is |
273 | | -called the *function declaration*: We declare, that there |
| 273 | +called the *function declaration*: we declare that there |
274 | 274 | shall be a function of the given name and type. The second line |
275 | 275 | reads: "The result of invoking `maxBits8` should be `255`." |
276 | 276 | (As you can see, we can use integer literals for other integral |
|
0 commit comments