Merge pull request #82 from AeneasVerif/son/switch

Improve tuple projections and matches over integers in Lean

1 files changed, 4 insertions, 0 deletions

diff --git a/compiler/Main.ml b/compiler/Main.ml
index 0b8ec439..4a2d01dc 100644
--- a/compiler/Main.ml
+++ b/compiler/Main.ml
@@ -123,6 +123,10 @@ let () =
       ( "-split-fwd-back",
         Arg.Clear return_back_funs,
         " Split the forward and backward functions." );
+      ( "-tuple-nested-proj",
+        Arg.Set use_nested_tuple_projectors,
+        " Use nested projectors for tuples (e.g., (0, 1).snd.fst instead of \
+         (0, 1).1)." );
     ]
   in