File tree Expand file tree Collapse file tree 2 files changed +4
-4
lines changed Expand file tree Collapse file tree 2 files changed +4
-4
lines changed Original file line number Diff line number Diff line change @@ -38,7 +38,7 @@ the literal is suitable for the ``Fin n`` type. The restricted behaviour can be
38
38
observed in the REPL, where the failure to construct a valid proof is caught during
39
39
the type-checking phase and not at runtime:
40
40
41
- .. code-block ::
41
+ .. code-block :: idris
42
42
43
43
Main> the (Fin 3) 2
44
44
FS (FS FZ)
Original file line number Diff line number Diff line change @@ -85,14 +85,14 @@ If you need to escape characters you still can by using a ``\\`` followed by the
85
85
``# `` that you used for your string delimiters. In the following example we are using two
86
86
``# `` characters as our escape sequence and want to print a line return:
87
87
88
- .. code-block ::
88
+ .. code-block :: idris
89
89
90
90
markdownExample : String
91
91
markdownExample = ##"markdown titles look like this: \##n"# Title \##n body""##
92
92
93
93
This last example could be implemented by combining raw string literals with multiline strings:
94
94
95
- .. code-block ::
95
+ .. code-block :: idris
96
96
97
97
markdownExample : String
98
98
markdownExample = ##"""
@@ -111,7 +111,7 @@ programs that evaluate to strings with a string literals in order to avoid manua
111
111
the concatenation of those expressions. To use interpolated strings, use ``\{ `` to start an
112
112
interpolation slice in which you can write an idris expression. Close it with ``} ``
113
113
114
- .. code-block ::
114
+ .. code-block :: idris
115
115
116
116
print : Expr -> String
117
117
print (Var name expr) = "let \{name} = \{print expr}"
You can’t perform that action at this time.
0 commit comments