add link

Author: Alex Gryzlov

src/Imp.lidr

@@ -287,6 +287,9 @@ Qed.
 Using `try` and `;` together, we can get rid of the repetition in the proof that
 was bothering us a little while ago.
 
+\todo[inline]{Mention
+http://docs.idris-lang.org/en/latest/reference/misc.html#alternatives ?}
+
 ```coq
 Theorem optimize_0plus_sound': forall a,
   aeval (optimize_0plus a) = aeval a.