Progress on cursor inspector for pattern singleton elaboration

hazelgrove · Dec 27, 2024 · fdb8a5e · fdb8a5e
1 parent 7158c4a
commit fdb8a5e
Showing 1 changed file with 10 additions and 1 deletion.
diff --git a/src/haz3lweb/view/CursorInspector.re b/src/haz3lweb/view/CursorInspector.re
@@ -324,7 +324,16 @@ let rec pat_view =
       ])
     }
   | InHole(Common(error)) => div_err(common_err_view(cls, error))
-  | NotInHole(ok) => div_ok(common_ok_view(~auto_labels=labels, cls, ok))
+  | NotInHole(ok) =>
+    div_ok(
+      common_ok_view(
+        ~auto_labels=labels,
+        ~lifted_ty=?Option.map(_ => info.ty, info.elaboration_provenance),
+        ~sugar_info=?Option.map(snd, info.elaboration_provenance),
+        cls,
+        ok,
+      ),
+    )
   };
 };
 let typ_view = (cls: Cls.t, status: Info.status_typ) =>