From c5acdec26e4a05c40811a4f1fcd9c49aece13117 Mon Sep 17 00:00:00 2001
From: thomasporter522 <thomasporter2019@gmail.com>
Date: Thu, 15 Aug 2024 13:01:23 -0400
Subject: [PATCH 1/6] new forms

---
 src/haz3lcore/lang/Form.re | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/src/haz3lcore/lang/Form.re b/src/haz3lcore/lang/Form.re
index 7e505240aa..ba087312f1 100644
--- a/src/haz3lcore/lang/Form.re
+++ b/src/haz3lcore/lang/Form.re
@@ -106,6 +106,9 @@ let keywords = [
   "if",
   "then",
   "else",
+  "theorem",
+  "proof",
+  "forall",
 ];
 let reserved_keywords = ["of", "when", "with", "switch", "match"];
 let keyword_regexp = regexp("^(" ++ String.concat("|", keywords) ++ ")$");
@@ -301,6 +304,7 @@ let forms: list((string, t)) = [
   ("parens_exp", mk(ii, ["(", ")"], mk_op(Exp, [Exp]))),
   ("parens_pat", mk(ii, ["(", ")"], mk_op(Pat, [Pat]))),
   ("parens_typ", mk(ii, ["(", ")"], mk_op(Typ, [Typ]))),
+  ("prop-equals", mk(ii, ["{", "=", "}"], mk_op(Typ, [Exp, Exp]))),
   ("ap_exp_empty", mk(ii, ["()"], mk_post(P.ap, Exp, []))),
   ("ap_exp", mk(ii, ["(", ")"], mk_post(P.ap, Exp, [Exp]))),
   ("ap_pat", mk(ii, ["(", ")"], mk_post(P.ap, Pat, [Pat]))),
@@ -315,7 +319,8 @@ let forms: list((string, t)) = [
   ("fun_", mk(ds, ["fun", "->"], mk_pre(P.fun_, Exp, [Pat]))),
   ("fix", mk(ds, ["fix", "->"], mk_pre(P.fun_, Exp, [Pat]))),
   ("typfun", mk(ds, ["typfun", "->"], mk_pre(P.fun_, Exp, [TPat]))),
-  ("forall", mk(ds, ["forall", "->"], mk_pre(P.fun_, Typ, [TPat]))),
+  ("forall-type", mk(ds, ["type", "->"], mk_pre(P.fun_, Typ, [TPat]))),
+  ("forall-term", mk(ds, ["forall", "->"], mk_pre(P.fun_, Typ, [Pat]))),
   ("rec", mk(ds, ["rec", "->"], mk_pre(P.fun_, Typ, [TPat]))),
   (
     "rule",
@@ -329,6 +334,10 @@ let forms: list((string, t)) = [
   ("filter_debug", mk(ds, ["debug", "in"], mk_pre(P.let_, Exp, [Exp]))),
   // TRIPLE DELIMITERS
   ("let_", mk(ds, ["let", "=", "in"], mk_pre(P.let_, Exp, [Pat, Exp]))),
+  (
+    "theorem_",
+    mk(ds, ["theorem", "proof", "in"], mk_pre(P.let_, Exp, [Pat, Exp])),
+  ),
   (
     "type_alias",
     mk(ds, ["type", "=", "in"], mk_pre(P.let_, Exp, [TPat, Typ])),

From 9ccd1137856e9648d3fc4031d51918919e932bb3 Mon Sep 17 00:00:00 2001
From: thomasporter522 <thomasporter2019@gmail.com>
Date: Thu, 15 Aug 2024 14:24:56 -0400
Subject: [PATCH 2/6] added core language constructs

---
 src/haz3lcore/assistant/AssistantForms.re    |   2 +-
 src/haz3lcore/dynamics/Casts.re              |  15 +-
 src/haz3lcore/dynamics/DHExp.re              |   2 +
 src/haz3lcore/dynamics/Elaborator.re         |  45 +-
 src/haz3lcore/dynamics/FilterMatcher.re      |   4 +
 src/haz3lcore/dynamics/Substitution.re       |   9 +
 src/haz3lcore/dynamics/Transition.re         |  15 +-
 src/haz3lcore/dynamics/TypeAssignment.re     |  10 +-
 src/haz3lcore/dynamics/Unboxing.re           |   1 +
 src/haz3lcore/lang/term/Typ.re               |  91 +++-
 src/haz3lcore/statics/Info.re                |   2 +-
 src/haz3lcore/statics/MakeTerm.re            |   2 +-
 src/haz3lcore/statics/Mode.re                |   6 +-
 src/haz3lcore/statics/Statics.re             |  38 +-
 src/haz3lcore/statics/Term.re                |  10 +-
 src/haz3lcore/statics/TermBase.re            |  42 +-
 src/haz3lcore/zipper/EditorUtil.re           |   3 +
 src/haz3lschool/SyntaxTest.re                |  11 +
 src/haz3lweb/view/ExplainThis.re             | 473 ++++++++++++++++++-
 src/haz3lweb/view/Type.re                    |  16 +-
 src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re |   2 +
 src/haz3lweb/view/dhcode/layout/HTypDoc.re   |  20 +-
 22 files changed, 741 insertions(+), 78 deletions(-)

diff --git a/src/haz3lcore/assistant/AssistantForms.re b/src/haz3lcore/assistant/AssistantForms.re
index 928a159f4a..3a6ea0a9cf 100644
--- a/src/haz3lcore/assistant/AssistantForms.re
+++ b/src/haz3lcore/assistant/AssistantForms.re
@@ -27,7 +27,7 @@ module Typ = {
     ("fun" ++ leading_expander, Arrow(unk, unk) |> Typ.fresh),
     (
       "typfun" ++ leading_expander,
-      Forall(Var("") |> TPat.fresh, unk) |> Typ.fresh,
+      Type(Var("") |> TPat.fresh, unk) |> Typ.fresh,
     ),
     ("if" ++ leading_expander, unk),
     ("let" ++ leading_expander, unk),
diff --git a/src/haz3lcore/dynamics/Casts.re b/src/haz3lcore/dynamics/Casts.re
index 170d057e76..c1e156cc2e 100644
--- a/src/haz3lcore/dynamics/Casts.re
+++ b/src/haz3lcore/dynamics/Casts.re
@@ -32,10 +32,17 @@ let grounded_Arrow =
     Arrow(Unknown(Internal) |> Typ.temp, Unknown(Internal) |> Typ.temp)
     |> Typ.temp,
   );
+let grounded_Type =
+  NotGroundOrHole(
+    Type(EmptyHole |> TPat.fresh, Unknown(Internal) |> Typ.temp) |> Typ.temp,
+  );
 let grounded_Forall =
   NotGroundOrHole(
-    Forall(EmptyHole |> TPat.fresh, Unknown(Internal) |> Typ.temp)
-    |> Typ.temp,
+    Forall(EmptyHole |> Pat.fresh, Unknown(Internal) |> Typ.temp) |> Typ.temp,
+  );
+let grounded_Equals =
+  NotGroundOrHole(
+    Equals(EmptyHole |> Exp.fresh, EmptyHole |> Exp.fresh) |> Typ.temp,
   );
 let grounded_Prod = length =>
   NotGroundOrHole(
@@ -60,7 +67,7 @@ let rec ground_cases_of = (ty: Typ.t): ground_cases => {
   | String
   | Var(_)
   | Rec(_)
-  | Forall(_, {term: Unknown(_), _})
+  | Type(_, {term: Unknown(_), _})
   | Arrow({term: Unknown(_), _}, {term: Unknown(_), _})
   | List({term: Unknown(_), _}) => Ground
   | Parens(ty) => ground_cases_of(ty)
@@ -79,7 +86,9 @@ let rec ground_cases_of = (ty: Typ.t): ground_cases => {
     sm |> ConstructorMap.is_ground(is_hole)
       ? Ground : NotGroundOrHole(Sum(grounded_Sum()) |> Typ.temp)
   | Arrow(_, _) => grounded_Arrow
+  | Type(_) => grounded_Type
   | Forall(_) => grounded_Forall
+  | Equals(_) => grounded_Equals
   | List(_) => grounded_List
   | Ap(_) => failwith("type application in dynamics")
   };
diff --git a/src/haz3lcore/dynamics/DHExp.re b/src/haz3lcore/dynamics/DHExp.re
index f7651ba963..0293f9944c 100644
--- a/src/haz3lcore/dynamics/DHExp.re
+++ b/src/haz3lcore/dynamics/DHExp.re
@@ -52,6 +52,7 @@ let rec strip_casts =
         | Seq(_)
         | Filter(_)
         | Let(_)
+        | Theorem(_)
         | FixF(_)
         | TyAlias(_)
         | Fun(_)
@@ -120,6 +121,7 @@ let ty_subst = (s: Typ.t, tpat: TPat.t, exp: t): t => {
           | Closure(_)
           | Seq(_)
           | Let(_)
+          | Theorem(_)
           | Ap(_)
           | BuiltinFun(_)
           | BinOp(_)
diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re
index c1f3aa12d7..3e6ad52560 100644
--- a/src/haz3lcore/dynamics/Elaborator.re
+++ b/src/haz3lcore/dynamics/Elaborator.re
@@ -65,9 +65,9 @@ let elaborated_type = (m: Statics.Map.t, uexp: UExp.t): (Typ.t, Ctx.t, 'a) => {
       let (ty1, ty2) = Typ.matched_arrow(ctx, self_ty);
       Typ.Arrow(ty1, ty2) |> Typ.temp;
     | SynTypFun =>
-      let (tpat, ty) = Typ.matched_forall(ctx, self_ty);
+      let (tpat, ty) = Typ.matched_type(ctx, self_ty);
       let tpat = Option.value(tpat, ~default=TPat.fresh(EmptyHole));
-      Typ.Forall(tpat, ty) |> Typ.temp;
+      Typ.Type(tpat, ty) |> Typ.temp;
     // We need to remove the synswitches from this type.
     | Ana(ana_ty) => Typ.match_synswitch(ana_ty, self_ty)
     };
@@ -92,9 +92,9 @@ let elaborated_pat_type = (m: Statics.Map.t, upat: UPat.t): (Typ.t, Ctx.t) => {
       let (ty1, ty2) = Typ.matched_arrow(ctx, self_ty);
       Typ.Arrow(ty1, ty2) |> Typ.temp;
     | SynTypFun =>
-      let (tpat, ty) = Typ.matched_forall(ctx, self_ty);
+      let (tpat, ty) = Typ.matched_type(ctx, self_ty);
       let tpat = Option.value(tpat, ~default=TPat.fresh(EmptyHole));
-      Typ.Forall(tpat, ty) |> Typ.temp;
+      Typ.Type(tpat, ty) |> Typ.temp;
     | Ana(ana_ty) =>
       switch (prev_synswitch) {
       | None => ana_ty
@@ -273,7 +273,7 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => {
       let (e', tye) = elaborate(m, e);
       Exp.TypFun(tpat, e', name)
       |> rewrap
-      |> cast_from(Typ.Forall(tpat, tye) |> Typ.temp);
+      |> cast_from(Typ.Type(tpat, tye) |> Typ.temp);
     | Tuple(es) =>
       let (ds, tys) = List.map(elaborate(m), es) |> ListUtil.unzip;
       Exp.Tuple(ds) |> rewrap |> cast_from(Prod(tys) |> Typ.temp);
@@ -317,6 +317,39 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => {
         let fixf = FixF(p, fresh_cast(def, ty2, ty1), None) |> DHExp.fresh;
         Exp.Let(p, fixf, body) |> rewrap |> cast_from(ty);
       };
+    | Theorem(p, def, body) =>
+      let add_name: (option(string), DHExp.t) => DHExp.t = (
+        (name, exp) => {
+          let (term, rewrap) = DHExp.unwrap(exp);
+          switch (term) {
+          | Fun(p, e, ctx, _) => Fun(p, e, ctx, name) |> rewrap
+          | TypFun(tpat, e, _) => TypFun(tpat, e, name) |> rewrap
+          | _ => exp
+          };
+        }
+      );
+      let (p, ty1) = elaborate_pattern(m, p);
+      let is_recursive =
+        Statics.is_recursive(ctx, p, def, ty1)
+        && Pat.get_bindings(p)
+        |> Option.get
+        |> List.exists(f => VarMap.lookup(co_ctx, f) != None);
+      if (!is_recursive) {
+        let def = add_name(Pat.get_var(p), def);
+        let (def, ty2) = elaborate(m, def);
+        let (body, ty) = elaborate(m, body);
+        Exp.Theorem(p, fresh_cast(def, ty2, ty1), body)
+        |> rewrap
+        |> cast_from(ty);
+      } else {
+        // TODO: Add names to mutually recursive functions
+        // TODO: Don't add fixpoint if there already is one
+        let def = add_name(Option.map(s => s ++ "+", Pat.get_var(p)), def);
+        let (def, ty2) = elaborate(m, def);
+        let (body, ty) = elaborate(m, body);
+        let fixf = FixF(p, fresh_cast(def, ty2, ty1), None) |> DHExp.fresh;
+        Exp.Theorem(p, fixf, body) |> rewrap |> cast_from(ty);
+      };
     | FixF(p, e, env) =>
       let (p', typ) = elaborate_pattern(m, p);
       let (e', tye) = elaborate(m, e);
@@ -356,7 +389,7 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => {
       |> cast_from(Arrow(remaining_arg_ty, tyf2) |> Typ.temp);
     | TypAp(e, ut) =>
       let (e', tye) = elaborate(m, e);
-      let (tpat, tye') = Typ.matched_forall(ctx, tye);
+      let (tpat, tye') = Typ.matched_type(ctx, tye);
       let ut' = Typ.normalize(ctx, ut);
       let tye'' =
         Typ.subst(
diff --git a/src/haz3lcore/dynamics/FilterMatcher.re b/src/haz3lcore/dynamics/FilterMatcher.re
index fc70d83756..0cb6785f9b 100644
--- a/src/haz3lcore/dynamics/FilterMatcher.re
+++ b/src/haz3lcore/dynamics/FilterMatcher.re
@@ -198,6 +198,10 @@ let rec matches_exp =
       matches_pat(dp, fp) && matches_exp(d1, f1) && matches_exp(d2, f2)
     | (Let(_), _) => false
 
+    | (Theorem(dp, d1, d2), Theorem(fp, f1, f2)) =>
+      matches_pat(dp, fp) && matches_exp(d1, f1) && matches_exp(d2, f2)
+    | (Theorem(_), _) => false
+
     | (TypAp(d1, t1), TypAp(d2, t2)) =>
       matches_exp(d1, d2) && matches_typ(t1, t2)
     | (TypAp(_), _) => false
diff --git a/src/haz3lcore/dynamics/Substitution.re b/src/haz3lcore/dynamics/Substitution.re
index 5d918e520b..455d5b2485 100644
--- a/src/haz3lcore/dynamics/Substitution.re
+++ b/src/haz3lcore/dynamics/Substitution.re
@@ -18,6 +18,15 @@ let rec subst_var = (m, d1: DHExp.t, x: Var.t, d2: DHExp.t): DHExp.t => {
     let dbody = subst_var(m, d1, x, dbody);
     let filter = subst_var_filter(m, d1, x, filter);
     Filter(filter, dbody) |> rewrap;
+  | Theorem(dp, d3, d4) =>
+    let d3 = subst_var(m, d1, x, d3);
+    let d4 =
+      if (DHPat.binds_var(m, x, dp)) {
+        d4;
+      } else {
+        subst_var(m, d1, x, d4);
+      };
+    Theorem(dp, d3, d4) |> rewrap;
   | Let(dp, d3, d4) =>
     let d3 = subst_var(m, d1, x, d3);
     let d4 =
diff --git a/src/haz3lcore/dynamics/Transition.re b/src/haz3lcore/dynamics/Transition.re
index a54c9d18d8..ce467bd630 100644
--- a/src/haz3lcore/dynamics/Transition.re
+++ b/src/haz3lcore/dynamics/Transition.re
@@ -192,6 +192,17 @@ module Transition = (EV: EV_MODE) => {
         kind: LetBind,
         is_value: false,
       });
+    | Theorem(dp, d1, d2) =>
+      let. _ = otherwise(env, d1 => Theorem(dp, d1, d2) |> rewrap)
+      and. d1' =
+        req_final(req(state, env), d1 => Let1(dp, d1, d2) |> wrap_ctx, d1);
+      let.match env' = (env, matches(dp, d1'));
+      Step({
+        expr: Closure(env', d2) |> fresh,
+        state_update,
+        kind: LetBind,
+        is_value: false,
+      });
     | TypFun(_)
     | Fun(_, _, Some(_), _) =>
       let. _ = otherwise(env, d);
@@ -299,8 +310,8 @@ module Transition = (EV: EV_MODE) => {
         })
       | Cast(
           d'',
-          {term: Forall(tp1, _), _} as t1,
-          {term: Forall(tp2, _), _} as t2,
+          {term: Type(tp1, _), _} as t1,
+          {term: Type(tp2, _), _} as t2,
         ) =>
         /* Rule ITTApCast */
         Step({
diff --git a/src/haz3lcore/dynamics/TypeAssignment.re b/src/haz3lcore/dynamics/TypeAssignment.re
index f4979d94bf..c6a01a11f5 100644
--- a/src/haz3lcore/dynamics/TypeAssignment.re
+++ b/src/haz3lcore/dynamics/TypeAssignment.re
@@ -143,6 +143,10 @@ and typ_of_dhexp = (ctx: Ctx.t, m: Statics.Map.t, dh: DHExp.t): option(Typ.t) =>
     let* ty1 = typ_of_dhexp(ctx, m, de);
     let* ctx = dhpat_extend_ctx(dhp, ty1, ctx);
     typ_of_dhexp(ctx, m, db);
+  | Theorem(dhp, de, db) =>
+    let* ty1 = typ_of_dhexp(ctx, m, de);
+    let* ctx = dhpat_extend_ctx(dhp, ty1, ctx);
+    typ_of_dhexp(ctx, m, db);
   | FixF(dhp, d, env) =>
     let* ty_p = dhpat_synthesize(dhp, ctx);
     let* ctx =
@@ -167,13 +171,13 @@ and typ_of_dhexp = (ctx: Ctx.t, m: Statics.Map.t, dh: DHExp.t): option(Typ.t) =>
     let ctx =
       Ctx.extend_tvar(ctx, {name, id: TPat.rep_id(utpat), kind: Abstract});
     let* ty = typ_of_dhexp(ctx, m, d);
-    Some(Typ.Forall(utpat, ty) |> Typ.temp);
+    Some(Typ.Type(utpat, ty) |> Typ.temp);
   | TypFun(_, d, _) =>
     let* ty = typ_of_dhexp(ctx, m, d);
-    Some(Typ.Forall(Var("?") |> TPat.fresh, ty) |> Typ.temp);
+    Some(Typ.Type(Var("?") |> TPat.fresh, ty) |> Typ.temp);
   | TypAp(d, ty1) =>
     let* ty = typ_of_dhexp(ctx, m, d);
-    let* (name, ty2) = Typ.matched_forall_strict(ctx, ty);
+    let* (name, ty2) = Typ.matched_type_strict(ctx, ty);
     switch (name) {
     | Some(name) => Some(Typ.subst(ty1, name, ty2))
     | None => Some(ty2)
diff --git a/src/haz3lcore/dynamics/Unboxing.re b/src/haz3lcore/dynamics/Unboxing.re
index 400620026c..2952ab2724 100644
--- a/src/haz3lcore/dynamics/Unboxing.re
+++ b/src/haz3lcore/dynamics/Unboxing.re
@@ -177,6 +177,7 @@ let rec unbox: type a. (unbox_request(a), DHExp.t) => unboxed(a) =
         Invalid(_) | Undefined | EmptyHole | MultiHole(_) | DynamicErrorHole(_) |
         Var(_) |
         Let(_) |
+        Theorem(_) |
         Fun(_, _, _, None) |
         FixF(_) |
         TyAlias(_) |
diff --git a/src/haz3lcore/lang/term/Typ.re b/src/haz3lcore/lang/term/Typ.re
index 3cb7f47b3c..6cefff5713 100644
--- a/src/haz3lcore/lang/term/Typ.re
+++ b/src/haz3lcore/lang/term/Typ.re
@@ -21,7 +21,9 @@ type cls =
   | Parens
   | Ap
   | Rec
-  | Forall;
+  | Type
+  | Forall
+  | Equals;
 
 include TermBase.Typ;
 
@@ -59,7 +61,9 @@ let cls_of_term: term => cls =
   | Ap(_) => Ap
   | Sum(_) => Sum
   | Rec(_) => Rec
-  | Forall(_) => Forall;
+  | Type(_) => Type
+  | Forall(_) => Forall
+  | Equals(_) => Equals;
 
 let show_cls: cls => string =
   fun
@@ -81,7 +85,9 @@ let show_cls: cls => string =
   | Parens => "Parenthesized type"
   | Ap => "Constructor application"
   | Rec => "Recursive type"
-  | Forall => "Forall type";
+  | Type => "Type type"
+  | Forall => "Forall type"
+  | Equals => "Equals type";
 
 let rec is_arrow = (typ: t) => {
   switch (typ.term) {
@@ -97,15 +103,17 @@ let rec is_arrow = (typ: t) => {
   | Var(_)
   | Ap(_)
   | Sum(_)
+  | Type(_)
   | Forall(_)
+  | Equals(_)
   | Rec(_) => false
   };
 };
 
-let rec is_forall = (typ: t) => {
+let rec is_type = (typ: t) => {
   switch (typ.term) {
-  | Parens(typ) => is_forall(typ)
-  | Forall(_) => true
+  | Parens(typ) => is_type(typ)
+  | Type(_) => true
   | Unknown(_)
   | Int
   | Float
@@ -117,6 +125,8 @@ let rec is_forall = (typ: t) => {
   | Var(_)
   | Ap(_)
   | Sum(_)
+  | Forall(_)
+  | Equals(_)
   | Rec(_) => false
   };
 };
@@ -155,7 +165,8 @@ let rec free_vars = (~bound=[], ty: t): list(Var.t) =>
   | Int
   | Float
   | Bool
-  | String => []
+  | String
+  | Equals(_) => []
   | Ap(t1, t2) => free_vars(~bound, t1) @ free_vars(~bound, t2)
   | Var(v) => List.mem(v, bound) ? [] : [v]
   | Parens(ty) => free_vars(~bound, ty)
@@ -164,8 +175,9 @@ let rec free_vars = (~bound=[], ty: t): list(Var.t) =>
   | Sum(sm) => ConstructorMap.free_variables(free_vars(~bound), sm)
   | Prod(tys) => ListUtil.flat_map(free_vars(~bound), tys)
   | Rec(x, ty)
-  | Forall(x, ty) =>
+  | Type(x, ty) =>
     free_vars(~bound=(x |> TPat.tyvar_of_utpat |> Option.to_list) @ bound, ty)
+  | Forall(_, ty) => free_vars(~bound, ty)
   };
 
 let var_count = ref(0);
@@ -232,7 +244,8 @@ let rec join = (~resolve=false, ~fix, ctx: Ctx.t, ty1: t, ty2: t): option(t) =>
     let+ ty_body = join(~resolve, ~fix, ctx, ty1', ty2);
     Rec(tp1, ty_body) |> temp;
   | (Rec(_), _) => None
-  | (Forall(x1, ty1), Forall(x2, ty2)) =>
+  | (Type(x1, ty1), Type(x2, ty2)) =>
+    // Note(Thomas): should this ctx be extended with x2 instead?
     let ctx = Ctx.extend_dummy_tvar(ctx, x1);
     let ty1' =
       switch (TPat.tyvar_of_utpat(x2)) {
@@ -240,14 +253,22 @@ let rec join = (~resolve=false, ~fix, ctx: Ctx.t, ty1: t, ty2: t): option(t) =>
       | None => ty1
       };
     let+ ty_body = join(~resolve, ~fix, ctx, ty1', ty2);
-    Forall(x1, ty_body) |> temp;
+    Type(x1, ty_body) |> temp;
   /* Note for above: there is no danger of free variable capture as
      subst itself performs capture avoiding substitution. However this
      may generate internal type variable names that in corner cases can
      be exposed to the user. We preserve the variable name of the
      second type to preserve synthesized type variable names, which
      come from user annotations. */
+  // TODO(theorem): allow for alpha variation and pattern joining
+  | (Forall(x1, ty1), Forall(x2, ty2)) when x1 == x2 =>
+    let+ ty_body = join(~resolve, ~fix, ctx, ty1, ty2);
+    Forall(x1, ty_body) |> temp;
+  | (Equals(e1, e2), Equals(e3, e4)) when e1 == e3 && e2 == e4 =>
+    Some(Equals(e1, e2) |> temp)
+  | (Type(_), _) => None
   | (Forall(_), _) => None
+  | (Equals(_), _) => None
   | (Int, Int) => Some(ty1)
   | (Int, _) => None
   | (Float, Float) => Some(ty1)
@@ -294,7 +315,10 @@ let rec match_synswitch = (t1: t, t2: t) => {
   | (Var(_), _)
   | (Ap(_), _)
   | (Rec(_), _)
-  | (Forall(_), _) => t1
+  | (Forall(_), _)
+  | (Type(_), _)
+  // TODO(theorem): can this have a synswitch inside?
+  | (Equals(_), _) => t1
   // These might
   | (List(ty1), List(ty2)) => List(match_synswitch(ty1, ty2)) |> rewrap1
   | (List(_), _) => t1
@@ -360,8 +384,11 @@ let rec normalize = (ctx: Ctx.t, ty: t): t => {
        as in current implementation Recs do not occur in the
        surface syntax, so we won't try to jump to them. */
     Rec(tpat, normalize(Ctx.extend_dummy_tvar(ctx, tpat), ty)) |> rewrap
-  | Forall(name, ty) =>
-    Forall(name, normalize(Ctx.extend_dummy_tvar(ctx, name), ty)) |> rewrap
+  | Type(name, ty) =>
+    Type(name, normalize(Ctx.extend_dummy_tvar(ctx, name), ty)) |> rewrap
+  /* NOTE(theorem): I don't think the ctx needs to be exteded with name */
+  | Forall(name, ty) => Forall(name, normalize(ctx, ty)) |> rewrap
+  | Equals(e1, e2) => Equals(e1, e2) |> rewrap
   };
 };
 
@@ -380,16 +407,16 @@ let matched_arrow = (ctx, ty) =>
        ~default=(Unknown(Internal) |> temp, Unknown(Internal) |> temp),
      );
 
-let rec matched_forall_strict = (ctx, ty) =>
+let rec matched_type_strict = (ctx, ty) =>
   switch (term_of(weak_head_normalize(ctx, ty))) {
-  | Parens(ty) => matched_forall_strict(ctx, ty)
-  | Forall(t, ty) => Some((Some(t), ty))
+  | Parens(ty) => matched_type_strict(ctx, ty)
+  | Type(t, ty) => Some((Some(t), ty))
   | Unknown(SynSwitch) => Some((None, Unknown(SynSwitch) |> temp))
   | _ => None // (None, Unknown(Internal) |> temp)
   };
 
-let matched_forall = (ctx, ty) =>
-  matched_forall_strict(ctx, ty)
+let matched_type = (ctx, ty) =>
+  matched_type_strict(ctx, ty)
   |> Option.value(~default=(None, Unknown(Internal) |> temp));
 
 let rec matched_prod_strict = (ctx, length, ty) =>
@@ -479,13 +506,31 @@ let rec needs_parens = (ty: t): bool =>
   | Bool
   | Var(_) => false
   | Rec(_, _)
-  | Forall(_, _) => true
+  | Forall(_, _)
+  | Type(_, _) => true
+  | Equals(_) /* is already wrapped in {} */
   | List(_) => false /* is already wrapped in [] */
   | Arrow(_, _) => true
   | Prod(_)
   | Sum(_) => true /* disambiguate between (A + B) -> C and A + (B -> C) */
   };
 
+let pretty_print_exp = (e: TermBase.Exp.t): string =>
+  switch (IdTagged.term_of(e)) {
+  | _ => failwith("Unimplemented: pretty printing expressions")
+  /* TODO(theorem): this function needs to be completed, and perhaps relocated */
+  };
+
+let pretty_print_pat = (v: TermBase.Pat.t): string =>
+  switch (IdTagged.term_of(v)) {
+  | Var(x) => x
+  | Invalid(_)
+  | EmptyHole
+  | MultiHole(_) => "?"
+  | _ => failwith("Unimplemented: pretty printing patterns")
+  /* TODO(theorem): this function needs to be completed, and perhaps relocated */
+  };
+
 let pretty_print_tvar = (tv: TPat.t): string =>
   switch (IdTagged.term_of(tv)) {
   | Var(x) => x
@@ -528,8 +573,12 @@ let rec pretty_print = (ty: t): string =>
        )
     ++ ")"
   | Rec(tv, t) => "rec " ++ pretty_print_tvar(tv) ++ "->" ++ pretty_print(t)
-  | Forall(tv, t) =>
-    "forall " ++ pretty_print_tvar(tv) ++ "->" ++ pretty_print(t)
+  | Type(tv, t) =>
+    "type " ++ pretty_print_tvar(tv) ++ "->" ++ pretty_print(t)
+  | Forall(v, t) =>
+    "forall " ++ pretty_print_pat(v) ++ ". " ++ pretty_print(t)
+  | Equals(e1, e2) =>
+    "{" ++ pretty_print_exp(e1) ++ " = " ++ pretty_print_exp(e2) ++ "}"
   }
 and ctr_pretty_print =
   fun
diff --git a/src/haz3lcore/statics/Info.re b/src/haz3lcore/statics/Info.re
index 8aaaeaae3d..152f6982a1 100644
--- a/src/haz3lcore/statics/Info.re
+++ b/src/haz3lcore/statics/Info.re
@@ -339,7 +339,7 @@ let rec status_common =
     switch (
       Typ.join_fix(
         ctx,
-        Forall(Var("?") |> TPat.fresh, Unknown(Internal) |> Typ.temp)
+        Type(Var("?") |> TPat.fresh, Unknown(Internal) |> Typ.temp)
         |> Typ.temp,
         ty,
       )
diff --git a/src/haz3lcore/statics/MakeTerm.re b/src/haz3lcore/statics/MakeTerm.re
index 673af0bb89..bc0c2d8871 100644
--- a/src/haz3lcore/statics/MakeTerm.re
+++ b/src/haz3lcore/statics/MakeTerm.re
@@ -425,7 +425,7 @@ and typ_term: unsorted => (UTyp.term, list(Id.t)) = {
    * Thus `rec A -> Left(A) + Right(B)` get parsed as `rec A -> (Left(A) + Right(B))`
    * If this is below the case for sum, then it gets parsed as an invalid form. */
   | Pre(([(_id, (["forall", "->"], [TPat(tpat)]))], []), Typ(t)) =>
-    ret(Forall(tpat, t))
+    ret(Type(tpat, t))
   | Pre(([(_id, (["rec", "->"], [TPat(tpat)]))], []), Typ(t)) =>
     ret(Rec(tpat, t))
   | Pre(tiles, Typ({term: Sum(t0), ids, _})) as tm =>
diff --git a/src/haz3lcore/statics/Mode.re b/src/haz3lcore/statics/Mode.re
index 5a85dbecd9..7ff2d4a6a3 100644
--- a/src/haz3lcore/statics/Mode.re
+++ b/src/haz3lcore/statics/Mode.re
@@ -35,7 +35,7 @@ let ty_of: t => Typ.t =
     Arrow(Unknown(SynSwitch) |> Typ.temp, Unknown(SynSwitch) |> Typ.temp)
     |> Typ.temp
   | SynTypFun =>
-    Forall(Var("syntypfun") |> TPat.fresh, Unknown(SynSwitch) |> Typ.temp)
+    Type(Var("syntypfun") |> TPat.fresh, Unknown(SynSwitch) |> Typ.temp)
     |> Typ.temp; /* TODO: naming the type variable? */
 
 let of_arrow = (ctx: Ctx.t, mode: t): (t, t) =>
@@ -46,13 +46,13 @@ let of_arrow = (ctx: Ctx.t, mode: t): (t, t) =>
   | Ana(ty) => ty |> Typ.matched_arrow(ctx) |> TupleUtil.map2(ana)
   };
 
-let of_forall = (ctx: Ctx.t, name_opt: option(string), mode: t): t =>
+let of_type = (ctx: Ctx.t, name_opt: option(string), mode: t): t =>
   switch (mode) {
   | Syn
   | SynFun
   | SynTypFun => Syn
   | Ana(ty) =>
-    let (name_expected_opt, item) = Typ.matched_forall(ctx, ty);
+    let (name_expected_opt, item) = Typ.matched_type(ctx, ty);
     switch (name_opt, name_expected_opt) {
     | (Some(name), Some(name_expected)) =>
       Ana(Typ.subst(Var(name) |> Typ.temp, name_expected, item))
diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re
index 2bb472edf9..95767f6944 100644
--- a/src/haz3lcore/statics/Statics.re
+++ b/src/haz3lcore/statics/Statics.re
@@ -59,7 +59,7 @@ let rec is_arrow_like = (t: Typ.t) => {
   switch (t |> Typ.term_of) {
   | Unknown(_) => true
   | Arrow(_) => true
-  | Forall(_, t) => is_arrow_like(t)
+  | Type(_, t) => is_arrow_like(t)
   | _ => false
   };
 };
@@ -341,7 +341,7 @@ and uexp_to_info_map =
     let typfn_mode = Mode.typap_mode;
     let (fn, m) = go(~mode=typfn_mode, fn, m);
     let (_, m) = utyp_to_info_map(~ctx, ~ancestors, utyp, m);
-    let (option_name, ty_body) = Typ.matched_forall(ctx, fn.ty);
+    let (option_name, ty_body) = Typ.matched_type(ctx, fn.ty);
     switch (option_name) {
     | Some(name) =>
       add(~self=Just(Typ.subst(utyp, name, ty_body)), ~co_ctx=fn.co_ctx, m)
@@ -375,25 +375,26 @@ and uexp_to_info_map =
     add'(~self, ~co_ctx=CoCtx.mk(ctx, p.ctx, e.co_ctx), m);
   | TypFun({term: Var(name), _} as utpat, body, _)
       when !Ctx.shadows_typ(ctx, name) =>
-    let mode_body = Mode.of_forall(ctx, Some(name), mode);
+    let mode_body = Mode.of_type(ctx, Some(name), mode);
     let m = utpat_to_info_map(~ctx, ~ancestors, utpat, m) |> snd;
     let ctx_body =
       Ctx.extend_tvar(ctx, {name, id: TPat.rep_id(utpat), kind: Abstract});
     let (body, m) = go'(~ctx=ctx_body, ~mode=mode_body, body, m);
     add(
-      ~self=Just(Forall(utpat, body.ty) |> Typ.temp),
+      ~self=Just(Type(utpat, body.ty) |> Typ.temp),
       ~co_ctx=body.co_ctx,
       m,
     );
   | TypFun(utpat, body, _) =>
-    let mode_body = Mode.of_forall(ctx, None, mode);
+    let mode_body = Mode.of_type(ctx, None, mode);
     let m = utpat_to_info_map(~ctx, ~ancestors, utpat, m) |> snd;
     let (body, m) = go(~mode=mode_body, body, m);
     add(
-      ~self=Just(Forall(utpat, body.ty) |> Typ.temp),
+      ~self=Just(Type(utpat, body.ty) |> Typ.temp),
       ~co_ctx=body.co_ctx,
       m,
     );
+  | Theorem(p, def, body)
   | Let(p, def, body) =>
     let (p_syn, _) =
       go_pat(~is_synswitch=true, ~co_ctx=CoCtx.empty, ~mode=Syn, p, m);
@@ -831,6 +832,9 @@ and utyp_to_info_map =
     (info, add_info(ids, InfoTyp(info), m));
   };
   let ancestors = [UTyp.rep_id(utyp)] @ ancestors;
+  let go_exp' = uexp_to_info_map(~ancestors);
+  let go_exp = go_exp'(~ctx);
+  let go_pat = upat_to_info_map(~ctx, ~ancestors);
   let go' = utyp_to_info_map(~ctx, ~ancestors);
   let go = go'(~expects=TypeExpected);
   //TODO(andrew): make this return free, replacing Typ.free_vars
@@ -877,7 +881,7 @@ and utyp_to_info_map =
         variants,
       );
     add(m);
-  | Forall({term: Var(name), _} as utpat, tbody) =>
+  | Type({term: Var(name), _} as utpat, tbody) =>
     let body_ctx =
       Ctx.extend_tvar(ctx, {name, id: TPat.rep_id(utpat), kind: Abstract});
     let m =
@@ -891,7 +895,7 @@ and utyp_to_info_map =
       |> snd;
     let m = utpat_to_info_map(~ctx, ~ancestors, utpat, m) |> snd;
     add(m); // TODO: check with andrew
-  | Forall(utpat, tbody) =>
+  | Type(utpat, tbody) =>
     let m =
       utyp_to_info_map(tbody, ~ctx, ~ancestors, ~expects=TypeExpected, m)
       |> snd;
@@ -917,6 +921,24 @@ and utyp_to_info_map =
       |> snd;
     let m = utpat_to_info_map(~ctx, ~ancestors, utpat, m) |> snd;
     add(m); // TODO: check with andrew
+  | Forall(p, tbody) =>
+    let (p', m) =
+      go_pat(~is_synswitch=false, ~co_ctx=CoCtx.empty, ~mode=Syn, p, m);
+    let m =
+      utyp_to_info_map(
+        tbody,
+        ~ctx=p'.ctx,
+        ~ancestors,
+        ~expects=TypeExpected,
+        m,
+      )
+      |> snd;
+    add(m);
+  | Equals(e1, e2) =>
+    let (e1, m) = go_exp(~mode=Syn, e1, m);
+    let (_, m) = go_exp'(~ctx=e1.ctx, ~mode=Syn, e2, m);
+    // TODO: constrain synthesized types to be equal
+    add(m);
   };
 }
 and utpat_to_info_map =
diff --git a/src/haz3lcore/statics/Term.re b/src/haz3lcore/statics/Term.re
index 0493150865..de810d47bf 100644
--- a/src/haz3lcore/statics/Term.re
+++ b/src/haz3lcore/statics/Term.re
@@ -100,7 +100,7 @@ module Pat = {
     switch (pat.term) {
     | Parens(pat) => is_fun_var(pat)
     | Cast(pat, typ, _) =>
-      is_var(pat) && (UTyp.is_arrow(typ) || Typ.is_forall(typ))
+      is_var(pat) && (UTyp.is_arrow(typ) || Typ.is_type(typ))
     | Invalid(_)
     | EmptyHole
     | MultiHole(_)
@@ -189,7 +189,7 @@ module Pat = {
     switch (pat.term) {
     | Parens(pat) => get_fun_var(pat)
     | Cast(pat, t1, _) =>
-      if (Typ.is_arrow(t1) || UTyp.is_forall(t1)) {
+      if (Typ.is_arrow(t1) || UTyp.is_type(t1)) {
         get_var(pat) |> Option.map(var => var);
       } else {
         None;
@@ -298,6 +298,7 @@ module Exp = {
     | Var
     | MetaVar
     | Let
+    | Theorem
     | FixF
     | TyAlias
     | Ap
@@ -348,6 +349,7 @@ module Exp = {
     | Tuple(_) => Tuple
     | Var(_) => Var
     | Let(_) => Let
+    | Theorem(_) => Theorem
     | FixF(_) => FixF
     | TyAlias(_) => TyAlias
     | Ap(_) => Ap
@@ -389,6 +391,7 @@ module Exp = {
     | Var => "Variable reference"
     | MetaVar => "Meta variable reference"
     | Let => "Let expression"
+    | Theorem => "Theorem expression"
     | FixF => "Fixpoint operator"
     | TyAlias => "Type Alias definition"
     | Ap => "Application"
@@ -433,6 +436,7 @@ module Exp = {
     | Tuple(_)
     | Var(_)
     | Let(_)
+    | Theorem(_)
     | FixF(_)
     | TyAlias(_)
     | Ap(_)
@@ -477,6 +481,7 @@ module Exp = {
       | BuiltinFun(_)
       | Var(_)
       | Let(_)
+      | Theorem(_)
       | FixF(_)
       | TyAlias(_)
       | Ap(_)
@@ -535,6 +540,7 @@ module Exp = {
       | TypFun(_)
       | Var(_)
       | Let(_)
+      | Theorem(_)
       | Filter(_)
       | TyAlias(_)
       | Ap(_)
diff --git a/src/haz3lcore/statics/TermBase.re b/src/haz3lcore/statics/TermBase.re
index f0585955c6..dd47cf3670 100644
--- a/src/haz3lcore/statics/TermBase.re
+++ b/src/haz3lcore/statics/TermBase.re
@@ -156,6 +156,7 @@ and Exp: {
     | Tuple(list(t))
     | Var(Var.t)
     | Let(Pat.t, t, t)
+    | Theorem(Pat.t, t, t)
     | FixF(Pat.t, t, option(ClosureEnvironment.t))
     | TyAlias(TPat.t, Typ.t, t)
     | Ap(Operators.ap_direction, t, t)
@@ -223,6 +224,7 @@ and Exp: {
     | Tuple(list(t))
     | Var(Var.t)
     | Let(Pat.t, t, t)
+    | Theorem(Pat.t, t, t)
     | FixF(Pat.t, t, [@show.opaque] option(ClosureEnvironment.t))
     | TyAlias(TPat.t, Typ.t, t)
     | Ap(Operators.ap_direction, t, t) // note: function is always first then argument; even in pipe mode
@@ -296,6 +298,8 @@ and Exp: {
         | Tuple(xs) => Tuple(List.map(exp_map_term, xs))
         | Let(p, e1, e2) =>
           Let(pat_map_term(p), exp_map_term(e1), exp_map_term(e2))
+        | Theorem(p, e1, e2) =>
+          Theorem(pat_map_term(p), exp_map_term(e1), exp_map_term(e2))
         | FixF(p, e, env) => FixF(pat_map_term(p), exp_map_term(e), env)
         | TyAlias(tp, t, e) =>
           TyAlias(tpat_map_term(tp), typ_map_term(t), exp_map_term(e))
@@ -366,6 +370,8 @@ and Exp: {
     | (Var(v1), Var(v2)) => v1 == v2
     | (Let(p1, e1, e2), Let(p2, e3, e4)) =>
       Pat.fast_equal(p1, p2) && fast_equal(e1, e3) && fast_equal(e2, e4)
+    | (Theorem(p1, e1, e2), Theorem(p2, e3, e4)) =>
+      Pat.fast_equal(p1, p2) && fast_equal(e1, e3) && fast_equal(e2, e4)
     | (FixF(p1, e1, c1), FixF(p2, e2, c2)) =>
       Pat.fast_equal(p1, p2)
       && fast_equal(e1, e2)
@@ -424,6 +430,7 @@ and Exp: {
     | (Tuple(_), _)
     | (Var(_), _)
     | (Let(_), _)
+    | (Theorem(_), _)
     | (FixF(_), _)
     | (TyAlias(_), _)
     | (Ap(_), _)
@@ -618,7 +625,9 @@ and Typ: {
     | Parens(t)
     | Ap(t, t)
     | Rec(TPat.t, t)
-    | Forall(TPat.t, t)
+    | Type(TPat.t, t)
+    | Forall(Pat.t, t)
+    | Equals(Exp.t, Exp.t)
   and t = IdTagged.t(term);
 
   type sum_map = ConstructorMap.t(t);
@@ -670,7 +679,9 @@ and Typ: {
     | Parens(t)
     | Ap(t, t)
     | Rec(TPat.t, t)
-    | Forall(TPat.t, t)
+    | Type(TPat.t, t)
+    | Forall(Pat.t, t)
+    | Equals(Exp.t, Exp.t)
   and t = IdTagged.t(term);
 
   type sum_map = ConstructorMap.t(t);
@@ -685,10 +696,14 @@ and Typ: {
         ~f_any=continue,
         x,
       ) => {
+    let exp_map_term =
+      Exp.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, ~f_rul, ~f_any);
     let typ_map_term =
       Typ.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, ~f_rul, ~f_any);
     let any_map_term =
       Any.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, ~f_rul, ~f_any);
+    let pat_map_term =
+      Pat.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, ~f_rul, ~f_any);
     let tpat_map_term =
       TPat.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, ~f_rul, ~f_any);
     let rec_call = ({term, _} as exp: t) => {
@@ -723,7 +738,9 @@ and Typ: {
             ),
           )
         | Rec(tp, t) => Rec(tpat_map_term(tp), typ_map_term(t))
-        | Forall(tp, t) => Forall(tpat_map_term(tp), typ_map_term(t))
+        | Type(tp, t) => Type(tpat_map_term(tp), typ_map_term(t))
+        | Forall(tp, t) => Forall(pat_map_term(tp), typ_map_term(t))
+        | Equals(e1, e2) => Equals(exp_map_term(e1), exp_map_term(e2))
         },
     };
     x |> f_typ(rec_call);
@@ -744,10 +761,13 @@ and Typ: {
       | Prod(tys) => Prod(List.map(subst(s, x), tys)) |> rewrap
       | Sum(sm) =>
         Sum(ConstructorMap.map(Option.map(subst(s, x)), sm)) |> rewrap
-      | Forall(tp2, ty)
+      | Type(tp2, ty)
           when TPat.tyvar_of_utpat(x) == TPat.tyvar_of_utpat(tp2) =>
-        Forall(tp2, ty) |> rewrap
-      | Forall(tp2, ty) => Forall(tp2, subst(s, x, ty)) |> rewrap
+        Type(tp2, ty) |> rewrap
+      | Type(tp2, ty) => Type(tp2, subst(s, x, ty)) |> rewrap
+      | Forall(p2, ty) => Forall(p2, subst(s, x, ty)) |> rewrap
+      // TODO: substitute into types in the term - requires helper for subst on expressions
+      | Equals(e1, e2) => Equals(e1, e2) |> rewrap
       | Rec(tp2, ty) when TPat.tyvar_of_utpat(x) == TPat.tyvar_of_utpat(tp2) =>
         Rec(tp2, ty) |> rewrap
       | Rec(tp2, ty) => Rec(tp2, subst(s, x, ty)) |> rewrap
@@ -768,7 +788,7 @@ and Typ: {
     | (Parens(t1), _) => eq_internal(n, t1, t2)
     | (_, Parens(t2)) => eq_internal(n, t1, t2)
     | (Rec(x1, t1), Rec(x2, t2))
-    | (Forall(x1, t1), Forall(x2, t2)) =>
+    | (Type(x1, t1), Type(x2, t2)) =>
       let alpha_subst =
         subst({
           term: Var("=" ++ string_of_int(n)),
@@ -777,7 +797,7 @@ and Typ: {
         });
       eq_internal(n + 1, alpha_subst(x1, t1), alpha_subst(x2, t2));
     | (Rec(_), _) => false
-    | (Forall(_), _) => false
+    | (Type(_), _) => false
     | (Int, Int) => true
     | (Int, _) => false
     | (Float, Float) => true
@@ -804,6 +824,12 @@ and Typ: {
     | (Sum(_), _) => false
     | (Var(n1), Var(n2)) => n1 == n2
     | (Var(_), _) => false
+    // TODO(theorem): improve these two comparisons
+    | (Equals(e1, e2), Equals(e3, e4)) when e1 == e3 && e2 == e4 => true
+    | (Equals(_), _) => false
+    | (Forall(p1, t1), Forall(p2, t2)) =>
+      p1 == p2 && eq_internal(n, t1, t2)
+    | (Forall(_), _) => false
     };
   };
 
diff --git a/src/haz3lcore/zipper/EditorUtil.re b/src/haz3lcore/zipper/EditorUtil.re
index ff59e48f55..1ad011ef75 100644
--- a/src/haz3lcore/zipper/EditorUtil.re
+++ b/src/haz3lcore/zipper/EditorUtil.re
@@ -42,6 +42,9 @@ let rec append_exp = (e1: Exp.t, e2: Exp.t): Exp.t => {
     | Let(p, edef, ebody) =>
       let ebody' = append_exp(ebody, e2);
       {ids: e1.ids, copied: false, term: Let(p, edef, ebody')};
+    | Theorem(p, edef, ebody) =>
+      let ebody' = append_exp(ebody, e2);
+      {ids: e1.ids, copied: false, term: Theorem(p, edef, ebody')};
     | TyAlias(tp, tdef, ebody) =>
       let ebody' = append_exp(ebody, e2);
       {ids: e1.ids, copied: false, term: TyAlias(tp, tdef, ebody')};
diff --git a/src/haz3lschool/SyntaxTest.re b/src/haz3lschool/SyntaxTest.re
index 23dff72251..e6e663553e 100644
--- a/src/haz3lschool/SyntaxTest.re
+++ b/src/haz3lschool/SyntaxTest.re
@@ -85,6 +85,8 @@ let rec find_fn =
   switch (uexp.term) {
   | Let(up, def, body) =>
     l |> find_in_let(name, up, def) |> find_fn(name, body)
+  | Theorem(up, def, body) =>
+    l |> find_in_let(name, up, def) |> find_fn(name, body)
   | ListLit(ul)
   | Tuple(ul) =>
     List.fold_left((acc, u1) => {find_fn(name, u1, acc)}, l, ul)
@@ -188,6 +190,9 @@ let rec var_mention = (name: string, uexp: Exp.t): bool => {
   | Let(p, def, body) =>
     var_mention_upat(name, p)
       ? false : var_mention(name, def) || var_mention(name, body)
+  | Theorem(p, def, body) =>
+    var_mention_upat(name, p)
+      ? false : var_mention(name, def) || var_mention(name, body)
   | TypFun(_, u, _)
   | TypAp(u, _)
   | Test(u)
@@ -250,6 +255,9 @@ let rec var_applied = (name: string, uexp: Exp.t): bool => {
   | Let(p, def, body) =>
     var_mention_upat(name, p)
       ? false : var_applied(name, def) || var_applied(name, body)
+  | Theorem(p, def, body) =>
+    var_mention_upat(name, p)
+      ? false : var_applied(name, def) || var_applied(name, body)
   | TypFun(_, u, _)
   | Test(u)
   | Parens(u)
@@ -339,6 +347,9 @@ let rec tail_check = (name: string, uexp: Exp.t): bool => {
   | Let(p, def, body) =>
     var_mention_upat(name, p) || var_mention(name, def)
       ? false : tail_check(name, body)
+  | Theorem(p, def, body) =>
+    var_mention_upat(name, p) || var_mention(name, def)
+      ? false : tail_check(name, body)
   | ListLit(l)
   | Tuple(l) =>
     //If l has no recursive calls then true
diff --git a/src/haz3lweb/view/ExplainThis.re b/src/haz3lweb/view/ExplainThis.re
index 0fb1efae04..a51d2acc76 100644
--- a/src/haz3lweb/view/ExplainThis.re
+++ b/src/haz3lweb/view/ExplainThis.re
@@ -1565,6 +1565,445 @@ let get_doc =
         | Parens(_) => default // Shouldn't get hit?
         | Cast(_) => default // Shouldn't get hit?
         };
+      | Theorem(pat, def, body) =>
+        let pat = bypass_parens_and_annot_pat(pat);
+        let pat_id = List.nth(pat.ids, 0);
+        let def_id = List.nth(def.ids, 0);
+        let body_id = List.nth(body.ids, 0);
+        let basic = group_id => {
+          get_message(
+            ~colorings=LetExp.let_base_exp_coloring_ids(~pat_id, ~def_id),
+            ~format=
+              Some(
+                msg =>
+                  Printf.sprintf(
+                    Scanf.format_from_string(msg, "%s%s"),
+                    Id.to_string(def_id),
+                    Id.to_string(pat_id),
+                  ),
+              ),
+            group_id,
+          );
+        };
+        switch (pat.term) {
+        | EmptyHole =>
+          if (LetExp.let_empty_hole_exp.id
+              == get_specificity_level(LetExp.lets_emptyhole)) {
+            get_message(
+              ~colorings=
+                LetExp.let_empty_hole_exp_coloring_ids(~pat_id, ~def_id),
+              ~format=
+                Some(
+                  msg =>
+                    Printf.sprintf(
+                      Scanf.format_from_string(msg, "%s%s%s"),
+                      Id.to_string(pat_id),
+                      Id.to_string(def_id),
+                      Id.to_string(pat_id),
+                    ),
+                ),
+              LetExp.lets_emptyhole,
+            );
+          } else {
+            basic(LetExp.lets_emptyhole);
+          }
+        | MultiHole(_) =>
+          if (LetExp.let_multi_hole_exp.id
+              == get_specificity_level(LetExp.lets_mutlihole)) {
+            get_message(
+              ~colorings=
+                LetExp.let_multi_hole_exp_coloring_ids(~pat_id, ~def_id),
+              ~format=
+                Some(
+                  msg =>
+                    Printf.sprintf(
+                      Scanf.format_from_string(msg, "%s%s%s"),
+                      Id.to_string(pat_id),
+                      Id.to_string(def_id),
+                      Id.to_string(pat_id),
+                    ),
+                ),
+              LetExp.lets_mutlihole,
+            );
+          } else {
+            basic(LetExp.lets_mutlihole);
+          }
+        | Wild =>
+          if (LetExp.let_wild_exp.id
+              == get_specificity_level(LetExp.lets_wild)) {
+            get_message(
+              ~colorings=LetExp.let_wild_exp_coloring_ids(~def_id, ~body_id),
+              ~format=
+                Some(
+                  msg =>
+                    Printf.sprintf(
+                      Scanf.format_from_string(msg, "%s%s%s"),
+                      Id.to_string(def_id),
+                      Id.to_string(def_id),
+                      Id.to_string(body_id),
+                    ),
+                ),
+              LetExp.lets_wild,
+            );
+          } else {
+            basic(LetExp.lets_wild);
+          }
+        | Int(i) =>
+          if (LetExp.let_int_exp.id == get_specificity_level(LetExp.lets_int)) {
+            get_message(
+              ~colorings=
+                LetExp.let_int_exp_coloring_ids(~pat_id, ~def_id, ~body_id),
+              ~format=
+                Some(
+                  msg =>
+                    Printf.sprintf(
+                      Scanf.format_from_string(msg, "%s%s%s%s%s"),
+                      Id.to_string(def_id),
+                      Id.to_string(pat_id),
+                      string_of_int(i),
+                      Id.to_string(def_id),
+                      Id.to_string(body_id),
+                    ),
+                ),
+              LetExp.lets_int,
+            );
+          } else {
+            /* TODO The coloring for the syntactic form is sometimes wrong here and some other places when switching between forms and specificity levels... maybe a Safari issue... */
+            basic(
+              LetExp.lets_int,
+            );
+          }
+        | Float(f) =>
+          if (LetExp.let_float_exp.id
+              == get_specificity_level(LetExp.lets_float)) {
+            // TODO Make sure everywhere printing the float literal print it prettier
+            get_message(
+              ~colorings=
+                LetExp.let_float_exp_coloring_ids(~pat_id, ~def_id, ~body_id),
+              ~format=
+                Some(
+                  msg =>
+                    Printf.sprintf(
+                      Scanf.format_from_string(msg, "%s%s%f%s%s"),
+                      Id.to_string(def_id),
+                      Id.to_string(pat_id),
+                      f,
+                      Id.to_string(def_id),
+                      Id.to_string(body_id),
+                    ),
+                ),
+              LetExp.lets_float,
+            );
+          } else {
+            /* TODO The coloring for the syntactic form is sometimes wrong here... */
+            basic(
+              LetExp.lets_float,
+            );
+          }
+        | Bool(b) =>
+          if (LetExp.let_bool_exp.id
+              == get_specificity_level(LetExp.lets_bool)) {
+            get_message(
+              ~colorings=
+                LetExp.let_bool_exp_coloring_ids(~pat_id, ~def_id, ~body_id),
+              ~format=
+                Some(
+                  msg =>
+                    Printf.sprintf(
+                      Scanf.format_from_string(msg, "%s%s%b%s%s"),
+                      Id.to_string(def_id),
+                      Id.to_string(pat_id),
+                      b,
+                      Id.to_string(def_id),
+                      Id.to_string(body_id),
+                    ),
+                ),
+              LetExp.lets_bool,
+            );
+          } else {
+            /* TODO The coloring for the syntactic form is sometimes wrong here... */
+            basic(
+              LetExp.lets_bool,
+            );
+          }
+        | String(s) =>
+          if (LetExp.let_str_exp.id == get_specificity_level(LetExp.lets_str)) {
+            get_message(
+              ~colorings=
+                LetExp.let_str_exp_coloring_ids(~pat_id, ~def_id, ~body_id),
+              ~format=
+                Some(
+                  msg =>
+                    Printf.sprintf(
+                      Scanf.format_from_string(msg, "%s%s%s%s%s"),
+                      Id.to_string(def_id),
+                      Id.to_string(pat_id),
+                      s,
+                      Id.to_string(def_id),
+                      Id.to_string(body_id),
+                    ),
+                ),
+              LetExp.lets_str,
+            );
+          } else {
+            /* TODO The coloring for the syntactic form is sometimes wrong here... */
+            basic(
+              LetExp.lets_str,
+            );
+          }
+        | Tuple([]) =>
+          if (LetExp.let_triv_exp.id
+              == get_specificity_level(LetExp.lets_triv)) {
+            get_message(
+              ~colorings=
+                LetExp.let_triv_exp_coloring_ids(~pat_id, ~def_id, ~body_id),
+              ~format=
+                Some(
+                  msg =>
+                    Printf.sprintf(
+                      Scanf.format_from_string(msg, "%s%s%s%s"),
+                      Id.to_string(def_id),
+                      Id.to_string(pat_id),
+                      Id.to_string(def_id),
+                      Id.to_string(body_id),
+                    ),
+                ),
+              LetExp.lets_triv,
+            );
+          } else {
+            /* TODO The coloring for the syntactic form is sometimes wrong here and other places when switching syntactic specificities... seems like might be Safari issue... */
+            basic(
+              LetExp.lets_triv,
+            );
+          }
+        | ListLit(elements) =>
+          if (List.length(elements) == 0) {
+            if (LetExp.let_listnil_exp.id
+                == get_specificity_level(LetExp.lets_listnil)) {
+              get_message(
+                ~colorings=
+                  LetExp.let_listnil_exp_coloring_ids(
+                    ~pat_id,
+                    ~def_id,
+                    ~body_id,
+                  ),
+                ~format=
+                  Some(
+                    msg =>
+                      Printf.sprintf(
+                        Scanf.format_from_string(msg, "%s%s%s%s"),
+                        Id.to_string(def_id),
+                        Id.to_string(pat_id),
+                        Id.to_string(def_id),
+                        Id.to_string(body_id),
+                      ),
+                  ),
+                LetExp.lets_listnil,
+              );
+            } else {
+              basic(LetExp.lets_listnil);
+            };
+          } else if (LetExp.let_listlit_exp.id
+                     == get_specificity_level(LetExp.lets_listlit)) {
+            get_message(
+              ~colorings=
+                LetExp.let_listlit_exp_coloring_ids(~pat_id, ~def_id),
+              ~format=
+                Some(
+                  msg =>
+                    Printf.sprintf(
+                      Scanf.format_from_string(msg, "%s%s%s"),
+                      Id.to_string(def_id),
+                      Id.to_string(pat_id),
+                      string_of_int(List.length(elements)),
+                    ),
+                ),
+              LetExp.lets_listlit,
+            );
+          } else {
+            basic(LetExp.lets_listlit);
+          }
+        | Cons(hd, tl) =>
+          if (LetExp.let_cons_exp.id
+              == get_specificity_level(LetExp.lets_cons)) {
+            let hd_id = List.nth(hd.ids, 0);
+            let tl_id = List.nth(tl.ids, 0);
+            get_message(
+              ~colorings=
+                LetExp.let_cons_exp_coloring_ids(~hd_id, ~tl_id, ~def_id),
+              ~format=
+                Some(
+                  msg =>
+                    Printf.sprintf(
+                      Scanf.format_from_string(msg, "%s%s%s"),
+                      Id.to_string(def_id),
+                      Id.to_string(hd_id),
+                      Id.to_string(tl_id),
+                    ),
+                ),
+              LetExp.lets_cons,
+            );
+          } else {
+            basic(LetExp.lets_cons);
+          }
+        | Var(var) =>
+          if (LetExp.let_var_exp.id == get_specificity_level(LetExp.lets_var)) {
+            get_message(
+              ~colorings=
+                LetExp.let_var_exp_coloring_ids(~pat_id, ~def_id, ~body_id),
+              ~format=
+                Some(
+                  msg =>
+                    Printf.sprintf(
+                      Scanf.format_from_string(msg, "%s%s%s%s"),
+                      Id.to_string(def_id),
+                      Id.to_string(pat_id),
+                      var,
+                      Id.to_string(body_id),
+                    ),
+                ),
+              LetExp.lets_var,
+            );
+          } else {
+            basic(LetExp.lets_var);
+          }
+        | Tuple(elements) =>
+          let basic_tuple = group_id => {
+            get_message(
+              ~colorings=LetExp.let_tuple_exp_coloring_ids(~pat_id, ~def_id),
+              ~format=
+                Some(
+                  msg =>
+                    Printf.sprintf(
+                      Scanf.format_from_string(msg, "%s%s%s"),
+                      Id.to_string(def_id),
+                      Id.to_string(pat_id),
+                      string_of_int(List.length(elements)),
+                    ),
+                ),
+              group_id,
+            );
+          };
+
+          switch (List.length(elements)) {
+          | 2 =>
+            let doc_id = get_specificity_level(LetExp.lets_tuple2);
+            if (LetExp.let_tuple2_exp.id == doc_id) {
+              let pat1_id = List.nth(List.nth(elements, 0).ids, 0);
+              let pat2_id = List.nth(List.nth(elements, 1).ids, 0);
+              get_message(
+                ~colorings=
+                  LetExp.let_tuple2_exp_coloring_ids(
+                    ~pat1_id,
+                    ~pat2_id,
+                    ~def_id,
+                  ),
+                ~format=
+                  Some(
+                    msg =>
+                      Printf.sprintf(
+                        Scanf.format_from_string(msg, "%s%s%s"),
+                        Id.to_string(def_id),
+                        Id.to_string(pat1_id),
+                        Id.to_string(pat2_id),
+                      ),
+                  ),
+                LetExp.lets_tuple2,
+              );
+            } else if (LetExp.let_tuple_exp.id == doc_id) {
+              basic_tuple(LetExp.lets_tuple2);
+            } else {
+              basic(LetExp.lets_tuple2);
+            };
+          | 3 =>
+            let doc_id = get_specificity_level(LetExp.lets_tuple3);
+            // TODO Syntactic form can go off page - so can examples - but can scroll, just can't see bottom scroll bar
+            if (LetExp.let_tuple3_exp.id == doc_id) {
+              let pat1_id = List.nth(List.nth(elements, 0).ids, 0);
+              let pat2_id = List.nth(List.nth(elements, 1).ids, 0);
+              let pat3_id = List.nth(List.nth(elements, 2).ids, 0);
+              get_message(
+                ~colorings=
+                  LetExp.let_tuple3_exp_coloring_ids(
+                    ~pat1_id,
+                    ~pat2_id,
+                    ~pat3_id,
+                    ~def_id,
+                  ),
+                ~format=
+                  Some(
+                    msg =>
+                      Printf.sprintf(
+                        Scanf.format_from_string(msg, "%s%s%s%s"),
+                        Id.to_string(def_id),
+                        Id.to_string(pat1_id),
+                        Id.to_string(pat2_id),
+                        Id.to_string(pat3_id),
+                      ),
+                  ),
+                LetExp.lets_tuple3,
+              );
+            } else if (LetExp.let_tuple_exp.id == doc_id) {
+              basic_tuple(LetExp.lets_tuple3);
+            } else {
+              basic(LetExp.lets_tuple3);
+            };
+          | _ =>
+            if (LetExp.let_tuple_exp.id
+                == get_specificity_level(LetExp.lets_tuple)) {
+              basic_tuple(LetExp.lets_tuple);
+            } else {
+              basic(LetExp.lets_tuple);
+            }
+          };
+        | Ap(con, arg) =>
+          if (LetExp.let_ap_exp.id == get_specificity_level(LetExp.lets_ap)) {
+            let con_id = List.nth(con.ids, 0);
+            let arg_id = List.nth(arg.ids, 0);
+            get_message(
+              ~colorings=
+                LetExp.let_ap_exp_coloring_ids(~con_id, ~arg_id, ~def_id),
+              ~format=
+                Some(
+                  msg =>
+                    Printf.sprintf(
+                      Scanf.format_from_string(msg, "%s%s%s"),
+                      Id.to_string(def_id),
+                      Id.to_string(con_id),
+                      Id.to_string(arg_id),
+                    ),
+                ),
+              LetExp.lets_ap,
+            );
+          } else {
+            basic(LetExp.lets_ap);
+          }
+        | Constructor(v, _) =>
+          if (LetExp.let_ctr_exp.id == get_specificity_level(LetExp.lets_ctr)) {
+            get_message(
+              ~colorings=
+                LetExp.let_ctr_exp_coloring_ids(~pat_id, ~def_id, ~body_id),
+              ~format=
+                Some(
+                  msg =>
+                    Printf.sprintf(
+                      Scanf.format_from_string(msg, "%s%s%s%s%s"),
+                      Id.to_string(def_id),
+                      Id.to_string(pat_id),
+                      v,
+                      Id.to_string(def_id),
+                      Id.to_string(body_id),
+                    ),
+                ),
+              LetExp.lets_ctr,
+            );
+          } else {
+            basic(LetExp.lets_ctr);
+          }
+        | Invalid(_) => default // Shouldn't get hit
+        | Parens(_) => default // Shouldn't get hit?
+        | Cast(_) => default // Shouldn't get hit?
+        };
       | FixF(pat, body, _) =>
         message_single(
           FixFExp.single(
@@ -2151,22 +2590,24 @@ let get_doc =
           ),
         ListTyp.list,
       );
-    | Forall(tpat, typ) =>
-      let tpat_id = List.nth(tpat.ids, 0);
-      let tbody_id = List.nth(typ.ids, 0);
-      get_message(
-        ~colorings=ForallTyp.forall_typ_coloring_ids(~tpat_id, ~tbody_id),
-        ~format=
-          Some(
-            msg =>
-              Printf.sprintf(
-                Scanf.format_from_string(msg, "%s%s"),
-                Id.to_string(tpat_id),
-                Id.to_string(tbody_id),
-              ),
-          ),
-        ForallTyp.forall,
-      );
+    | Type(_, _) => get_message(TerminalExp.int_exps(0))
+    | Forall(_, _) => get_message(TerminalExp.int_exps(0))
+    | Equals(_, _) => get_message(TerminalExp.int_exps(0))
+    // let tpat_id = List.nth(tpat.ids, 0);
+    // let tbody_id = List.nth(typ.ids, 0);
+    // get_message(
+    //   ~colorings=ForallTyp.forall_typ_coloring_ids(~tpat_id, ~tbody_id),
+    //   ~format=
+    //     Some(
+    //       msg =>
+    //         Printf.sprintf(
+    //           Scanf.format_from_string(msg, "%s%s"),
+    //           Id.to_string(tpat_id),
+    //           Id.to_string(tbody_id),
+    //         ),
+    //     ),
+    //   ForallTyp.forall,
+    // );
     | Rec(tpat, typ) =>
       let tpat_id = List.nth(tpat.ids, 0);
       let tbody_id = List.nth(typ.ids, 0);
diff --git a/src/haz3lweb/view/Type.re b/src/haz3lweb/view/Type.re
index 4ee4f29af2..164567df3f 100644
--- a/src/haz3lweb/view/Type.re
+++ b/src/haz3lweb/view/Type.re
@@ -3,6 +3,12 @@ open Node;
 open Util.Web;
 open Haz3lcore;
 
+let pat_view = (pat: Haz3lcore.Pat.t): string =>
+  switch (pat.term) {
+  | Var(x) => x
+  | _ => "?"
+  };
+
 let tpat_view = (tpat: Haz3lcore.TPat.t): string =>
   switch (tpat.term) {
   | Var(x) => x
@@ -36,11 +42,19 @@ let rec view_ty = (~strip_outer_parens=false, ty: Haz3lcore.Typ.t): Node.t =>
       ~attrs=[clss(["typ-view", "Rec"])],
       [text("Rec " ++ tpat_view(name) ++ ". "), view_ty(t)],
     )
+  | Type(name, t) =>
+    div(
+      ~attrs=[clss(["typ-view", "Type"])],
+      [text("type " ++ tpat_view(name) ++ " -> "), view_ty(t)],
+    )
   | Forall(name, t) =>
     div(
       ~attrs=[clss(["typ-view", "Forall"])],
-      [text("forall " ++ tpat_view(name) ++ " -> "), view_ty(t)],
+      [text("forall " ++ pat_view(name) ++ " -> "), view_ty(t)],
     )
+  | Equals(_, _) =>
+    // TODO: view expressions
+    div(~attrs=[clss(["typ-view", "Equals"])], [text("{ ... = ... }")])
   | List(t) =>
     div(
       ~attrs=[clss(["typ-view", "atom", "List"])],
diff --git a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re
index 34efdf0735..f35bf99163 100644
--- a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re
+++ b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re
@@ -75,6 +75,7 @@ let rec precedence = (~show_casts: bool, d: DHExp.t) => {
   | TypFun(_)
   | Fun(_) => DHDoc_common.precedence_max
   | Let(_)
+  | Theorem(_)
   | TyAlias(_)
   | FixF(_)
   | Match(_) => DHDoc_common.precedence_max
@@ -419,6 +420,7 @@ let mk =
       | Cast(d, _, _) =>
         let doc = go'(d);
         doc;
+      | Theorem(dp, ddef, dbody)
       | Let(dp, ddef, dbody) =>
         if (enforce_inline) {
           fail();
diff --git a/src/haz3lweb/view/dhcode/layout/HTypDoc.re b/src/haz3lweb/view/dhcode/layout/HTypDoc.re
index 996d01f607..4e0562d108 100644
--- a/src/haz3lweb/view/dhcode/layout/HTypDoc.re
+++ b/src/haz3lweb/view/dhcode/layout/HTypDoc.re
@@ -20,13 +20,15 @@ let precedence = (ty: Typ.t): int =>
   | String
   | Unknown(_)
   | Var(_)
+  | Type(_)
   | Forall(_)
   | Rec(_)
   | Sum(_) => precedence_Sum
   | List(_) => precedence_Const
   | Prod(_) => precedence_Prod
   | Arrow(_, _) => precedence_Arrow
-  | Parens(_) => precedence_Const
+  | Parens(_)
+  | Equals(_) => precedence_Const
   | Ap(_) => precedence_Ap
   };
 
@@ -136,9 +138,21 @@ let rec mk = (~parenthesize=false, ~enforce_inline: bool, ty: Typ.t): t => {
         ]),
         parenthesize,
       )
+    | Type(name, ty) => (
+        hcats([
+          text("type " ++ Type.tpat_view(name) ++ "->{"),
+          (
+            (~enforce_inline) =>
+              annot(HTypAnnot.Step(0), mk(~enforce_inline, ty))
+          )
+          |> pad_child(~enforce_inline),
+          mk_delim("}"),
+        ]),
+        parenthesize,
+      )
     | Forall(name, ty) => (
         hcats([
-          text("forall " ++ Type.tpat_view(name) ++ "->{"),
+          text("forall " ++ Type.pat_view(name) ++ "->{"),
           (
             (~enforce_inline) =>
               annot(HTypAnnot.Step(0), mk(~enforce_inline, ty))
@@ -148,6 +162,8 @@ let rec mk = (~parenthesize=false, ~enforce_inline: bool, ty: Typ.t): t => {
         ]),
         parenthesize,
       )
+    // TODO: display expressions
+    | Equals(_, _) => (hcats([text("{ ... = ... }")]), parenthesize)
     | Sum(sum_map) =>
       let center =
         List.mapi(

From 3e662de01ab6c72131c3ba84d5ef3eeba6c472fd Mon Sep 17 00:00:00 2001
From: thomasporter522 <thomasporter2019@gmail.com>
Date: Thu, 15 Aug 2024 14:56:31 -0400
Subject: [PATCH 3/6] fixed form name

---
 src/haz3lcore/lang/Form.re                 | 2 +-
 src/haz3lweb/explainthis/Example.re        | 2 +-
 src/haz3lweb/explainthis/data/ForallTyp.re | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/haz3lcore/lang/Form.re b/src/haz3lcore/lang/Form.re
index ba087312f1..3b54941c15 100644
--- a/src/haz3lcore/lang/Form.re
+++ b/src/haz3lcore/lang/Form.re
@@ -346,7 +346,7 @@ let forms: list((string, t)) = [
 ];
 
 let get: String.t => t =
-  name => Util.ListUtil.assoc_err(name, forms, "Forms.get");
+  name => Util.ListUtil.assoc_err(name, forms, "Form.get: " ++ name);
 
 let delims: list(Token.t) =
   forms
diff --git a/src/haz3lweb/explainthis/Example.re b/src/haz3lweb/explainthis/Example.re
index 9408167cf6..0c8f9dc41e 100644
--- a/src/haz3lweb/explainthis/Example.re
+++ b/src/haz3lweb/explainthis/Example.re
@@ -68,7 +68,7 @@ let mk_parens_typ = mk_tile(Form.get("parens_typ"));
 let mk_list_exp = mk_tile(Form.get("list_lit_exp"));
 let mk_list_pat = mk_tile(Form.get("list_lit_pat"));
 let mk_list_typ = mk_tile(Form.get("list_typ"));
-let mk_forall = mk_tile(Form.get("forall"));
+let mk_type = mk_tile(Form.get("forall-type"));
 let mk_rec = mk_tile(Form.get("rec"));
 let arrow = () => mk_monotile(Form.get("type-arrow"));
 let unary_minus = () => mk_monotile(Form.get("unary_minus"));
diff --git a/src/haz3lweb/explainthis/data/ForallTyp.re b/src/haz3lweb/explainthis/data/ForallTyp.re
index 09eca4e576..ee013e6243 100644
--- a/src/haz3lweb/explainthis/data/ForallTyp.re
+++ b/src/haz3lweb/explainthis/data/ForallTyp.re
@@ -13,7 +13,7 @@ let forall_typ: form = {
   let explanation = "This forall type classifies polymorphic values varying over [*type variable*](%s) with [*instantiated type*](%s).";
   {
     id: ForallTyp,
-    syntactic_form: [mk_forall([[space(), _tpat, space()]]), _typ_arg],
+    syntactic_form: [mk_type([[space(), _tpat, space()]]), _typ_arg],
     expandable_id: Some((Piece.id(_tpat), [_typ_arg])),
     explanation,
     examples: [],

From 809b9d94b894a265045cd65f89e0329259b3e77c Mon Sep 17 00:00:00 2001
From: thomasporter522 <thomasporter2019@gmail.com>
Date: Fri, 16 Aug 2024 12:04:57 -0400
Subject: [PATCH 4/6] added maketerm cases, causing stack overflow

---
 src/haz3lcore/statics/MakeTerm.re | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/haz3lcore/statics/MakeTerm.re b/src/haz3lcore/statics/MakeTerm.re
index bc0c2d8871..037ad9e45e 100644
--- a/src/haz3lcore/statics/MakeTerm.re
+++ b/src/haz3lcore/statics/MakeTerm.re
@@ -220,6 +220,8 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = {
         | (["fix", "->"], [Pat(pat)]) => FixF(pat, r, None)
         | (["typfun", "->"], [TPat(tpat)]) => TypFun(tpat, r, None)
         | (["let", "=", "in"], [Pat(pat), Exp(def)]) => Let(pat, def, r)
+        | (["theorem", "proof", "in"], [Pat(pat), Exp(def)]) =>
+          Theorem(pat, def, r)
         | (["hide", "in"], [Exp(filter)]) =>
           Filter(Filter({act: (Eval, One), pat: filter}), r)
         | (["eval", "in"], [Exp(filter)]) =>
@@ -409,6 +411,7 @@ and typ_term: unsorted => (UTyp.term, list(Id.t)) = {
         | ([t], []) when Form.is_typ_var(t) => Var(t)
         | (["(", ")"], [Typ(body)]) => Parens(body)
         | (["[", "]"], [Typ(body)]) => List(body)
+        | (["{", "=", "}"], [Exp(e1), Exp(e2)]) => Equals(e1, e2)
         | ([t], []) when t != " " && !Form.is_explicit_hole(t) =>
           Unknown(Hole(Invalid(t)))
         | _ => hole(tm)
@@ -424,8 +427,10 @@ and typ_term: unsorted => (UTyp.term, list(Id.t)) = {
   /* forall and rec have to be before sum so that they bind tighter.
    * Thus `rec A -> Left(A) + Right(B)` get parsed as `rec A -> (Left(A) + Right(B))`
    * If this is below the case for sum, then it gets parsed as an invalid form. */
-  | Pre(([(_id, (["forall", "->"], [TPat(tpat)]))], []), Typ(t)) =>
+  | Pre(([(_id, (["type", "->"], [TPat(tpat)]))], []), Typ(t)) =>
     ret(Type(tpat, t))
+  | Pre(([(_id, (["forall", "->"], [Pat(pat)]))], []), Typ(t)) =>
+    ret(Forall(pat, t))
   | Pre(([(_id, (["rec", "->"], [TPat(tpat)]))], []), Typ(t)) =>
     ret(Rec(tpat, t))
   | Pre(tiles, Typ({term: Sum(t0), ids, _})) as tm =>

From 07e19e5f29c88598779dbf8cb75adcf4d31cb55e Mon Sep 17 00:00:00 2001
From: thomasporter522 <thomasporter2019@gmail.com>
Date: Mon, 19 Aug 2024 11:58:22 -0400
Subject: [PATCH 5/6] added ground cases, fixed stack overflow

---
 src/haz3lcore/dynamics/Casts.re | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/haz3lcore/dynamics/Casts.re b/src/haz3lcore/dynamics/Casts.re
index c1e156cc2e..0ef9728b55 100644
--- a/src/haz3lcore/dynamics/Casts.re
+++ b/src/haz3lcore/dynamics/Casts.re
@@ -68,6 +68,8 @@ let rec ground_cases_of = (ty: Typ.t): ground_cases => {
   | Var(_)
   | Rec(_)
   | Type(_, {term: Unknown(_), _})
+  | Forall(_, {term: Unknown(_), _})
+  | Equals({term: EmptyHole, _}, {term: EmptyHole, _})
   | Arrow({term: Unknown(_), _}, {term: Unknown(_), _})
   | List({term: Unknown(_), _}) => Ground
   | Parens(ty) => ground_cases_of(ty)

From da408484b15b5efd372c3fdf2b936c2c46d29514 Mon Sep 17 00:00:00 2001
From: thomasporter522 <thomasporter2019@gmail.com>
Date: Wed, 28 Aug 2024 15:55:40 -0400
Subject: [PATCH 6/6] Merge branch 'dev' of https://github.com/hazelgrove/hazel
 into theorem-keyword

---
 src/haz3lcore/dynamics/FilterMatcher.re | 50 +++++++++++++++++++++++++
 src/haz3lcore/lang/term/Typ.re          |  5 ++-
 2 files changed, 53 insertions(+), 2 deletions(-)

diff --git a/src/haz3lcore/dynamics/FilterMatcher.re b/src/haz3lcore/dynamics/FilterMatcher.re
index 30679fda1b..92a11a6748 100644
--- a/src/haz3lcore/dynamics/FilterMatcher.re
+++ b/src/haz3lcore/dynamics/FilterMatcher.re
@@ -375,6 +375,56 @@ and matches_fun =
   };
 }
 
+and matches_pat = (d: Pat.t, f: Pat.t): bool => {
+  switch (d |> DHPat.term_of, f |> DHPat.term_of) {
+  // Matt: I'm not sure what the exact semantics of matching should be here.
+  | (Parens(x), _) => matches_pat(x, f)
+  | (_, Parens(x)) => matches_pat(d, x)
+  | (Cast(x, _, _), _) => matches_pat(x, f)
+  | (_, Cast(x, _, _)) => matches_pat(d, x)
+  | (_, EmptyHole) => true
+  | (MultiHole(_), MultiHole(_)) => true
+  | (MultiHole(_), _) => false
+  | (Wild, Wild) => true
+  | (Wild, _) => false
+  | (Int(dv), Int(fv)) => dv == fv
+  | (Int(_), _) => false
+  | (Float(dv), Float(fv)) => dv == fv
+  | (Float(_), _) => false
+  | (Bool(dv), Bool(fv)) => dv == fv
+  | (Bool(_), _) => false
+  | (String(dv), String(fv)) => dv == fv
+  | (String(_), _) => false
+  | (ListLit(dl), ListLit(fl)) =>
+    switch (
+      List.fold_left2((res, d, f) => res && matches_pat(d, f), true, dl, fl)
+    ) {
+    | exception (Invalid_argument(_)) => false
+    | res => res
+    }
+  | (ListLit(_), _) => false
+  | (Constructor(dt, _), Constructor(ft, _)) => dt == ft
+  | (Constructor(_), _) => false
+  | (Var(_), Var(_)) => true
+  | (Var(_), _) => false
+  | (Tuple(dl), Tuple(fl)) =>
+    switch (
+      List.fold_left2((res, d, f) => res && matches_pat(d, f), true, dl, fl)
+    ) {
+    | exception (Invalid_argument(_)) => false
+    | res => res
+    }
+  | (Tuple(_), _) => false
+  | (Ap(d1, d2), Ap(f1, f2)) => matches_pat(d1, f1) && matches_pat(d2, f2)
+  | (Ap(_), _) => false
+  | (Cons(d1, d2), Cons(f1, f2)) =>
+    matches_pat(d1, f1) && matches_pat(d2, f2)
+  | (Cons(_), _) => false
+  | (EmptyHole, _) => false
+  | (Invalid(_), _) => false
+  };
+}
+
 and matches_typ = (d: Typ.t, f: Typ.t) => {
   Typ.eq(d, f);
 }
diff --git a/src/haz3lcore/lang/term/Typ.re b/src/haz3lcore/lang/term/Typ.re
index c655b804f0..0f98f55248 100644
--- a/src/haz3lcore/lang/term/Typ.re
+++ b/src/haz3lcore/lang/term/Typ.re
@@ -573,9 +573,10 @@ let rec pretty_print = (ty: t): string =>
          ts,
        )
     ++ ")"
-  | Rec(tv, t) => "rec " ++ pretty_print_tvar(tv) ++ "->" ++ pretty_print(t)
+  | Rec(tv, t) =>
+    "rec " ++ pretty_print_tvar(tv) ++ " -> " ++ pretty_print(t)
   | Type(tv, t) =>
-    "type " ++ pretty_print_tvar(tv) ++ "->" ++ pretty_print(t)
+    "type " ++ pretty_print_tvar(tv) ++ " -> " ++ pretty_print(t)
   | Forall(v, t) =>
     "forall " ++ pretty_print_pat(v) ++ ". " ++ pretty_print(t)
   | Equals(e1, e2) =>