version select

hazelgrove · Oct 25, 2024 · a3931ec · a3931ec
1 parent 8e741b1
commit a3931ec
Show file tree

Hide file tree

Showing 26 changed files with 1,042 additions and 596 deletions.
diff --git a/src/haz3lcore/assistant/AssistantForms.re b/src/haz3lcore/assistant/AssistantForms.re
@@ -38,6 +38,10 @@ module Typ = {
     ("of_prop" ++ leading_expander, unk),
     ("of_alfa_exp" ++ leading_expander, unk),
     ("of_alfa_typ" ++ leading_expander, unk),
+    ("consistent" ++ leading_expander, unk),
+    ("matched_arrow" ++ leading_expander, unk),
+    ("matched_prod" ++ leading_expander, unk),
+    ("matched_sum" ++ leading_expander, unk),
     ("eval" ++ leading_expander, unk),
   ];
 

diff --git a/src/haz3lcore/derivation/DrvSyntax.re b/src/haz3lcore/derivation/DrvSyntax.re
@@ -271,9 +271,9 @@ let repr = (~sp: string=" ", p: int, syntax: t): Aba.t(string, t) => {
         ? "·" |> op_sg : List.init(List.length(ctx) - 1, _ => ",") |> bin
     | Entail(_) => "⊢" |> bin_sg
     | Consistent(_) => "~" |> bin_sg
-    | MatchedArrow(_) => "▶→" |> bin_sg
-    | MatchedProd(_) => "▶×" |> bin_sg
-    | MatchedSum(_) => "▶+" |> bin_sg
+    | MatchedArrow(_) => "▸→" |> bin_sg
+    | MatchedProd(_) => "▸×" |> bin_sg
+    | MatchedSum(_) => "▸+" |> bin_sg
     | NumLit(i) => string_of_int(i) |> op_sg
     | Val(_) => "val" |> post_sg
     | Neg(_) => "-" |> pre_sg