theorem now elaborates to in-part

hazelgrove · May 22, 2024 · 9546f78 · 9546f78
1 parent 50ca02d
commit 9546f78
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re
@@ -200,7 +200,7 @@ let rec dhexp_of_uexp =
       | Test(test) =>
         let+ dtest = dhexp_of_uexp(m, test);
         DHExp.Test(id, dtest);
-      | Theorem(_, _, _) => Some(DHExp.Tuple([]))
+      | Theorem(_, _, e) => dhexp_of_uexp(m, e)
       | Filter(act, cond, body) =>
         let* dcond = dhexp_of_uexp(~in_filter=true, m, cond);
         let+ dbody = dhexp_of_uexp(m, body);