@@ -272,6 +272,9 @@ elabCon info syn tn codata expkind (doc, argDocs, n, t_in, fc, forcenames)
272272
273273type EliminatorState = StateT (Map.Map String Int) Idris
274274
275+-- -- Issue #1616 in the issue tracker.
276+-- https://github.com/idris-lang/Idris-dev/issues/1616
277+--
275278-- TODO: Rewrite everything to use idris_implicits instead of manual splitting (or in TT)
276279-- FIXME: Many things have name starting with elim internally since this was the only purpose in the first edition of the function
277280-- rename to caseFun to match updated intend