Skip to content

Commit f54e45b

Browse files
authored
[ vim ] set syntax of md files to markdown (#55)
* [ vim ] set syntax of md files to markdown * [ lint ] fix terminology
1 parent 8b02a2d commit f54e45b

16 files changed

+21
-18
lines changed

src/Appendices/Neovim.md

+1-1
Original file line numberDiff line numberDiff line change
@@ -370,5 +370,5 @@ is available for some other editors, so feel free to ask what's
370370
available for your editor of choice, for instance on the
371371
[Idris 2 Discord channel](https://discord.gg/UX68fDs2jc).
372372

373-
<!-- vi: filetype=idris2
373+
<!-- vi: filetype=idris2:syntax=markdown
374374
-->

src/Appendices/Projects.md

+1-1
Original file line numberDiff line numberDiff line change
@@ -886,5 +886,5 @@ an Idris library or application. Finally, we learned how to include
886886
external libraries in an Idris project and how to use pack to help us
887887
keep track of these dependencies.
888888

889-
<!-- vi: filetype=idris2
889+
<!-- vi: filetype=idris2:syntax=markdown
890890
-->

src/Tutorial/DPair.md

+1-1
Original file line numberDiff line numberDiff line change
@@ -1202,5 +1202,5 @@ contracts between values hold. These will eventually allow
12021202
us to define pre- and post conditions for our function
12031203
arguments and output types.
12041204

1205-
<!-- vi: filetype=idris2
1205+
<!-- vi: filetype=idris2:syntax=markdown
12061206
-->

src/Tutorial/DataTypes.md

+1-1
Original file line numberDiff line numberDiff line change
@@ -1364,5 +1364,5 @@ already provided by the *Prelude*.
13641364
In the [next section](Interfaces.md), we will introduce
13651365
*interfaces*, another approach to *function overloading*.
13661366

1367-
<!-- vi: filetype=idris2
1367+
<!-- vi: filetype=idris2:syntax=markdown
13681368
-->

src/Tutorial/Dependent.md

+1-1
Original file line numberDiff line numberDiff line change
@@ -906,5 +906,5 @@ library. Likewise, `Fin` is available from `Data.Fin` from *base*.
906906
In the [next section](IO.md), it is time to learn how to write effectful programs
907907
and how to do this while still staying *pure*.
908908

909-
<!-- vi: filetype=idris2
909+
<!-- vi: filetype=idris2:syntax=markdown
910910
-->

src/Tutorial/Eq.md

+1-1
Original file line numberDiff line numberDiff line change
@@ -1094,5 +1094,5 @@ thus reducing the need to return a `Maybe` or other failure type,
10941094
because due to the restricted input, our functions can no longer
10951095
fail.
10961096

1097-
<!-- vi: filetype=idris2
1097+
<!-- vi: filetype=idris2:syntax=markdown
10981098
-->

src/Tutorial/Folds.md

+1-1
Original file line numberDiff line numberDiff line change
@@ -1060,5 +1060,5 @@ In the next chapter, we are taking the concept of iterating
10601060
over container types one step further and look at
10611061
effectful data traversals.
10621062

1063-
<!-- vi: filetype=idris2
1063+
<!-- vi: filetype=idris2:syntax=markdown
10641064
-->

src/Tutorial/Functions1.md

+1-1
Original file line numberDiff line numberDiff line change
@@ -579,5 +579,5 @@ our own data types and how to construct and deconstruct
579579
values of these new types. We will also learn about
580580
generic types and functions.
581581

582-
<!-- vi: filetype=idris2
582+
<!-- vi: filetype=idris2:syntax=markdown
583583
-->

src/Tutorial/Functions2.md

+2-2
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33
So far, we learned about the core features of the Idris
44
language, which it has in common with several other
55
pure, strongly typed programming languages like Haskell:
6-
(Higher order) Functions, algebraic data types, pattern matching,
6+
(Higher-order) Functions, algebraic data types, pattern matching,
77
parametric polymorphism (generic types and functions), and
88
ad hoc polymorphism (interfaces and constrained functions).
99

@@ -960,5 +960,5 @@ Idris' type signatures will be of paramount importance there. Whenever
960960
you feel lost, add one or more holes and inspect their context to decide what to
961961
do next.
962962

963-
<!-- vi: filetype=idris2
963+
<!-- vi: filetype=idris2:syntax=markdown
964964
-->

src/Tutorial/Functor.md

+1-1
Original file line numberDiff line numberDiff line change
@@ -1423,5 +1423,5 @@ In the [next chapter](Folds.md) we get to learn more about
14231423
recursion, totality checking, and an interface for
14241424
collapsing container types: `Foldable`.
14251425
1426-
<!-- vi: filetype=idris2
1426+
<!-- vi: filetype=idris2:syntax=markdown
14271427
-->

src/Tutorial/IO.md

+3-3
Original file line numberDiff line numberDiff line change
@@ -645,7 +645,7 @@ additional namespaces to modules. For instance, in order
645645
to define another function called `eval`, we need to add
646646
it to its own namespace (note, that all definitions in a
647647
namespace must be indented by the same amount of
648-
white space):
648+
whitespace):
649649

650650
```idris
651651
namespace Foo
@@ -684,7 +684,7 @@ Sometimes, even *do blocks* are too noisy to express a
684684
combination of effectful computations. In this case, we
685685
can prefix the effectful parts with an exclamation mark
686686
(wrapping them in parentheses if they contain additional
687-
white space), while leaving pure expressions unmodified:
687+
whitespace), while leaving pure expressions unmodified:
688688

689689
```idris
690690
getHello : IO ()
@@ -1121,5 +1121,5 @@ Now, that we had a glimpse at *monads* and the *bind* operator,
11211121
it is time to in the [next chapter](Functor.md) introduce `Monad` and some
11221122
related interfaces for real.
11231123

1124-
<!-- vi: filetype=idris2
1124+
<!-- vi: filetype=idris2:syntax=markdown
11251125
-->

src/Tutorial/Interfaces.md

+1-1
Original file line numberDiff line numberDiff line change
@@ -817,5 +817,5 @@ at functions and their types. We will learn about named arguments,
817817
implicit arguments, and erased arguments as well as some
818818
constructors for implementing more complex functions.
819819
820-
<!-- vi: filetype=idris2
820+
<!-- vi: filetype=idris2:syntax=markdown
821821
-->

src/Tutorial/Intro.md

+3
Original file line numberDiff line numberDiff line change
@@ -448,3 +448,6 @@ in Idris for real. We learn how to write our own pure
448448
functions, how functions compose, and how we can treat
449449
functions just like other values and pass them around
450450
as arguments to other functions.
451+
452+
<!-- vi: filetype=idris2:syntax=markdown
453+
-->

src/Tutorial/Predicates.md

+1-1
Original file line numberDiff line numberDiff line change
@@ -1365,5 +1365,5 @@ arguments, which Idris should try to construct on its own if
13651365
it has enough information about the structure of a function's
13661366
arguments.
13671367

1368-
<!-- vi: filetype=idris2
1368+
<!-- vi: filetype=idris2:syntax=markdown
13691369
-->

src/Tutorial/Prim.md

+1-1
Original file line numberDiff line numberDiff line change
@@ -1407,5 +1407,5 @@ things perform well at runtime and compile time. I'm experimenting
14071407
with a library, which deals with these issues. It is not yet finished,
14081408
but you can have a look at it [here](https://github.com/stefan-hoeck/idris2-prim).
14091409
1410-
<!-- vi: filetype=idris2
1410+
<!-- vi: filetype=idris2:syntax=markdown
14111411
-->

src/Tutorial/Traverse.md

+1-1
Original file line numberDiff line numberDiff line change
@@ -1144,5 +1144,5 @@ There's one still missing - `Alternative` - but this will
11441144
have to wait a bit longer, because we need to first make
11451145
our brains smoke with some more type-level wizardry.
11461146

1147-
<!-- vi: filetype=idris2
1147+
<!-- vi: filetype=idris2:syntax=markdown
11481148
-->

0 commit comments

Comments
 (0)