From f556423ae2c649b9d7fae35302579cda3db537f9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 25 Feb 2019 17:43:21 -0800
Subject: [PATCH] chore(library/compiler/llnf): add TODO

---
 src/library/compiler/llnf.cpp | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/src/library/compiler/llnf.cpp b/src/library/compiler/llnf.cpp
index 4d23fd9b29..e61bead4e9 100644
--- a/src/library/compiler/llnf.cpp
+++ b/src/library/compiler/llnf.cpp
@@ -557,7 +557,17 @@ class to_llnf_fn {
            ```
            @decidable.cases_on t _cnstr.0.0 _cnstr.1.0
            ```
-           which reduces to `t`. */
+           which reduces to `t`.
+
+           TODO(Leo): extend `is_id` when there multiple nested cases_on applications.
+           Example:
+           ```
+           @prod.cases_on _x_1 (λ fst snd,
+             @except.cases_on fst
+               (λ a, let _x_2 := except.error ◾ ◾ a in (_x_2, snd))
+               (λ a, let _x_3 := except.ok ◾ ◾ a in (_x_3, snd)))
+           ```
+        */
         bool is_id  = true;
         // bool all_eq = true;
         /* Process minor premises */