Skip to content

Commit 0a03935

Browse files
committed
Imp: fix link
1 parent a112706 commit 0a03935

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/Imp.lidr

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -290,7 +290,7 @@ Using `try` and `;` together, we can get rid of the repetition in the proof that
290290
was bothering us a little while ago.
291291
292292
\todo[inline]{Mention
293-
http://docs.idris-lang.org/en/latest/reference/misc.html#alternatives ?}
293+
\href{http://docs.idris-lang.org/en/latest/reference/misc.html\#alternatives}{Alternatives} ?}
294294
295295
```coq
296296
Theorem optimize_0plus_sound': forall a,

0 commit comments

Comments
 (0)