Skip to content

Commit 2ad7be7

Browse files
committed
Poly: fix some formatting issues
1 parent 3719da3 commit 2ad7be7

File tree

1 file changed

+6
-6
lines changed

1 file changed

+6
-6
lines changed

src/Poly.lidr

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -119,8 +119,8 @@ appropriate type parameter:
119119
> test_repeat2 = Refl
120120

121121

122-
\todo[inline]{Explain implicits and {x=foo} syntax first? Move after the
123-
"Supplying Type Arguments Explicitly" section?}
122+
\todo[inline]{Explain implicits and \idr{{x=foo}} syntax first? Move after the
123+
"Supplying Type Arguments Explicitly" section?}
124124

125125
==== Exercise: 2 starsM (mumble_grumble)
126126

@@ -187,8 +187,8 @@ code).
187187

188188
==== Type Argument Synthesis
189189

190-
\todo[inline]{We should mention the `_` parameters but it won't work like this
191-
in Idris}
190+
\todo[inline]{We should mention the \idr{_} parameters but it won't work like
191+
this in Idris}
192192

193193
To use a polymorphic function, we need to pass it one or more types in addition
194194
to its other arguments. For example, the recursive call in the body of the
@@ -570,8 +570,8 @@ For example, if we apply `filter` to the predicate `evenb` and a list of numbers
570570
> length_is_1 : (l : List x) -> Bool
571571
> length_is_1 l = beq_nat (length l) 1
572572

573-
\todo[inline]{Why doesn't this work without {x=Nat}? Apparently it even works
574-
with {x=_}!}
573+
\todo[inline]{Why doesn't this work without \idr{{x=Nat}}? Apparently it even
574+
works with \idr{{x=_}}!}
575575

576576
> test_filter2 : filter (length_is_1 {x=Nat})
577577
> [ [1,2], [3], [4], [5,6,7], [], [8] ]

0 commit comments

Comments
 (0)