From 6c8a7b6f5f7b01758989cfcd8784d27262570c0b Mon Sep 17 00:00:00 2001
From: GuoDCZ <richard_zhong@sjtu.edu.cn>
Date: Fri, 17 May 2024 00:40:15 -0400
Subject: [PATCH] task(2/7): prop pattern supported

---
 src/haz3lcore/assistant/AssistantForms.re     |  5 +-
 src/haz3lcore/dynamics/Builtins.re            | 21 +++++-
 src/haz3lcore/dynamics/DH.re                  | 13 ++++
 src/haz3lcore/dynamics/Elaborator.re          |  6 +-
 src/haz3lcore/dynamics/EvalCtx.re             |  6 ++
 src/haz3lcore/dynamics/EvaluatorError.re      |  1 +
 src/haz3lcore/dynamics/EvaluatorError.rei     |  1 +
 src/haz3lcore/dynamics/EvaluatorPost.re       | 14 ++++
 src/haz3lcore/dynamics/EvaluatorStep.re       |  6 ++
 src/haz3lcore/dynamics/FilterMatcher.re       |  9 +++
 src/haz3lcore/dynamics/PatternMatch.re        |  6 ++
 src/haz3lcore/dynamics/Stepper.re             |  7 ++
 src/haz3lcore/dynamics/Substitution.re        |  5 ++
 src/haz3lcore/dynamics/Transition.re          | 26 ++++++++
 src/haz3lcore/lang/Form.re                    |  4 ++
 src/haz3lcore/lang/Precedence.re              | 23 ++++---
 src/haz3lcore/statics/Derivation.re           | 34 ++++++++++
 src/haz3lcore/statics/MakeTerm.re             |  4 ++
 src/haz3lcore/statics/Statics.re              | 11 +++-
 src/haz3lcore/statics/Term.re                 | 20 +++++-
 src/haz3lcore/statics/TermBase.re             | 33 +++++++++-
 src/haz3lcore/statics/TypBase.re              | 10 +++
 src/haz3lcore/zipper/EditorUtil.re            |  1 +
 src/haz3lschool/SyntaxTest.re                 |  4 ++
 src/haz3lweb/explainthis/Example.re           |  3 +
 src/haz3lweb/explainthis/ExplainThisForm.re   |  4 ++
 src/haz3lweb/explainthis/data/OpExp.re        | 66 +++++++++++++++++++
 src/haz3lweb/explainthis/data/TerminalExp.re  | 12 ++++
 src/haz3lweb/explainthis/data/TerminalTyp.re  | 13 ++++
 src/haz3lweb/view/ExplainThis.re              |  5 ++
 src/haz3lweb/view/Type.re                     |  1 +
 src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re  | 21 ++++++
 .../view/dhcode/layout/DHDoc_common.re        |  5 ++
 .../view/dhcode/layout/DHDoc_common.rei       |  5 ++
 src/haz3lweb/view/dhcode/layout/HTypDoc.re    |  1 +
 35 files changed, 389 insertions(+), 17 deletions(-)

diff --git a/src/haz3lcore/assistant/AssistantForms.re b/src/haz3lcore/assistant/AssistantForms.re
index b9fb8bffa8..007c08a0d7 100644
--- a/src/haz3lcore/assistant/AssistantForms.re
+++ b/src/haz3lcore/assistant/AssistantForms.re
@@ -38,7 +38,6 @@ module Typ = {
     ("@", List(unk)),
     (";", unk),
     ("&&", Bool),
-    ("\\/", Bool),
     ("||", Bool),
     ("$==", Bool),
     ("==.", Bool),
@@ -65,6 +64,10 @@ module Typ = {
     ("/.", Float),
     ("**.", Float),
     ("++", String),
+    ("/\\", Prop),
+    ("\\/", Prop),
+    ("==>", Prop),
+    ("|-", Prop),
   ];
 
   let expected: Info.t => Typ.t =
diff --git a/src/haz3lcore/dynamics/Builtins.re b/src/haz3lcore/dynamics/Builtins.re
index aa77a4864a..faded377c9 100644
--- a/src/haz3lcore/dynamics/Builtins.re
+++ b/src/haz3lcore/dynamics/Builtins.re
@@ -239,6 +239,22 @@ module Pervasives = {
         | Tuple([PropLit(p1), PropLit(p2)]) => Ok(PropLit(Implies(p1, p2)))
         | d => Error(InvalidBoxedTuple(d)),
       );
+
+    let prop_of: DHExp.t => option(Derivation.Prop.t) =
+      fun
+      | PropLit(p) => Some(p)
+      | _ => None;
+
+    let entail =
+      unary(
+        fun
+        | Tuple([ListLit(_, _, Prop, ctx), PropLit(p)]) =>
+          switch (ctx |> List.map(prop_of) |> Util.OptUtil.sequence) {
+          | Some(ctx) => Ok(JudgementLit(Entail(ctx, p)))
+          | None => Error(InvalidBoxedListLit(List.hd(ctx)))
+          }
+        | d => Error(InvalidBoxedTuple(d)),
+      );
   };
 
   open Impls;
@@ -300,7 +316,10 @@ module Pervasives = {
     |> fn("atom", String, Prop, atom)
     |> fn("and", Prod([Prop, Prop]), Prop, and_)
     |> fn("or", Prod([Prop, Prop]), Prop, or_)
-    |> fn("implies", Prod([Prop, Prop]), Prop, implies);
+    |> fn("implies", Prod([Prop, Prop]), Prop, implies)
+    |> const("truth", Prop, PropLit(Truth))
+    |> const("falsity", Prop, PropLit(Falsity))
+    |> fn("entail", Prod([List(Prop), Prop]), Judgement, entail);
 };
 
 let ctx_init: Ctx.t = {
diff --git a/src/haz3lcore/dynamics/DH.re b/src/haz3lcore/dynamics/DH.re
index e4f2c4e5fa..9812e8cb29 100644
--- a/src/haz3lcore/dynamics/DH.re
+++ b/src/haz3lcore/dynamics/DH.re
@@ -30,10 +30,12 @@ module rec DHExp: {
     | FloatLit(float)
     | StringLit(string)
     | PropLit(Derivation.Prop.t)
+    | JudgementLit(Derivation.Judgement.t)
     | BinBoolOp(TermBase.UExp.op_bin_bool, t, t)
     | BinIntOp(TermBase.UExp.op_bin_int, t, t)
     | BinFloatOp(TermBase.UExp.op_bin_float, t, t)
     | BinStringOp(TermBase.UExp.op_bin_string, t, t)
+    | BinPropOp(TermBase.UExp.op_bin_prop, t, t)
     | ListLit(MetaVar.t, MetaVarInst.t, Typ.t, list(t))
     | Cons(t, t)
     | ListConcat(t, t)
@@ -88,10 +90,12 @@ module rec DHExp: {
     | FloatLit(float)
     | StringLit(string)
     | PropLit(Derivation.Prop.t)
+    | JudgementLit(Derivation.Judgement.t)
     | BinBoolOp(TermBase.UExp.op_bin_bool, t, t)
     | BinIntOp(TermBase.UExp.op_bin_int, t, t)
     | BinFloatOp(TermBase.UExp.op_bin_float, t, t)
     | BinStringOp(TermBase.UExp.op_bin_string, t, t)
+    | BinPropOp(TermBase.UExp.op_bin_prop, t, t)
     | ListLit(MetaVar.t, MetaVarInst.t, Typ.t, list(t))
     | Cons(t, t)
     | ListConcat(t, t)
@@ -131,10 +135,12 @@ module rec DHExp: {
     | FloatLit(_) => "FloatLit"
     | StringLit(_) => "StringLit"
     | PropLit(_) => "PropLit"
+    | JudgementLit(_) => "JudgementLit"
     | BinBoolOp(_, _, _) => "BinBoolOp"
     | BinIntOp(_, _, _) => "BinIntOp"
     | BinFloatOp(_, _, _) => "BinFloatOp"
     | BinStringOp(_, _, _) => "BinStringOp"
+    | BinPropOp(_, _, _) => "BinPropOp"
     | ListLit(_) => "ListLit"
     | Cons(_, _) => "Cons"
     | ListConcat(_, _) => "ListConcat"
@@ -190,6 +196,7 @@ module rec DHExp: {
     | BinFloatOp(a, b, c) => BinFloatOp(a, strip_casts(b), strip_casts(c))
     | BinStringOp(a, b, c) =>
       BinStringOp(a, strip_casts(b), strip_casts(c))
+    | BinPropOp(a, b, c) => BinPropOp(a, strip_casts(b), strip_casts(c))
     | ConsistentCase(Case(a, rs, b)) =>
       ConsistentCase(
         Case(strip_casts(a), List.map(strip_casts_rule, rs), b),
@@ -210,6 +217,7 @@ module rec DHExp: {
     | FloatLit(_) as d
     | StringLit(_) as d
     | PropLit(_) as d
+    | JudgementLit(_) as d
     | Constructor(_) as d
     | InvalidOperation(_) as d => d
     | IfThenElse(consistent, c, d1, d2) =>
@@ -234,6 +242,8 @@ module rec DHExp: {
     | (StringLit(_), _) => false
     | (PropLit(p1), PropLit(p2)) => Derivation.Prop.eq(p1, p2)
     | (PropLit(_), _) => false
+    | (JudgementLit(j1), JudgementLit(j2)) => Derivation.Judgement.eq(j1, j2)
+    | (JudgementLit(_), _) => false
 
     /* Non-hole forms: recurse */
     | (Test(id1, d1), Test(id2, d2)) => id1 == id2 && fast_equal(d1, d2)
@@ -269,6 +279,8 @@ module rec DHExp: {
       op1 == op2 && fast_equal(d11, d12) && fast_equal(d21, d22)
     | (BinStringOp(op1, d11, d21), BinStringOp(op2, d12, d22)) =>
       op1 == op2 && fast_equal(d11, d12) && fast_equal(d21, d22)
+    | (BinPropOp(op1, d11, d21), BinPropOp(op2, d12, d22)) =>
+      op1 == op2 && fast_equal(d11, d12) && fast_equal(d21, d22)
     | (Cast(d1, ty11, ty21), Cast(d2, ty12, ty22))
     | (FailedCast(d1, ty11, ty21), FailedCast(d2, ty12, ty22)) =>
       fast_equal(d1, d2) && ty11 == ty12 && ty21 == ty22
@@ -301,6 +313,7 @@ module rec DHExp: {
     | (BinIntOp(_), _)
     | (BinFloatOp(_), _)
     | (BinStringOp(_), _)
+    | (BinPropOp(_), _)
     | (Cast(_), _)
     | (FailedCast(_), _)
     | (InvalidOperation(_), _)
diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re
index 96701733e6..6454983d95 100644
--- a/src/haz3lcore/dynamics/Elaborator.re
+++ b/src/haz3lcore/dynamics/Elaborator.re
@@ -13,7 +13,8 @@ let exp_binop_of: Term.UExp.op_bin => (Typ.t, (_, _) => DHExp.t) =
   | Int(op) => (Int, ((e1, e2) => BinIntOp(op, e1, e2)))
   | Float(op) => (Float, ((e1, e2) => BinFloatOp(op, e1, e2)))
   | Bool(op) => (Bool, ((e1, e2) => BinBoolOp(op, e1, e2)))
-  | String(op) => (String, ((e1, e2) => BinStringOp(op, e1, e2)));
+  | String(op) => (String, ((e1, e2) => BinStringOp(op, e1, e2)))
+  | Prop(op) => (Prop, ((e1, e2) => BinPropOp(op, e1, e2)));
 
 let fixed_exp_typ = (m: Statics.Map.t, e: Term.UExp.t): option(Typ.t) =>
   switch (Id.Map.find_opt(Term.UExp.rep_id(e), m)) {
@@ -98,10 +99,12 @@ let cast = (ctx: Ctx.t, mode: Mode.t, self_ty: Typ.t, d: DHExp.t) =>
     | FloatLit(_)
     | StringLit(_)
     | PropLit(_)
+    | JudgementLit(_)
     | BinBoolOp(_)
     | BinIntOp(_)
     | BinFloatOp(_)
     | BinStringOp(_)
+    | BinPropOp(_)
     | Test(_) => DHExp.cast(d, self_ty, ana_ty)
     };
   };
@@ -146,6 +149,7 @@ let rec dhexp_of_uexp =
       | Float(n) => Some(FloatLit(n))
       | String(s) => Some(StringLit(s))
       | Prop(p) => Some(PropLit(p))
+      | Judgement(j) => Some(JudgementLit(j))
       | ListLit(es) =>
         let* ds = es |> List.map(dhexp_of_uexp(m)) |> OptUtil.sequence;
         let+ ty = fixed_exp_typ(m, uexp);
diff --git a/src/haz3lcore/dynamics/EvalCtx.re b/src/haz3lcore/dynamics/EvalCtx.re
index 85ba47f5dd..c47cbbc979 100644
--- a/src/haz3lcore/dynamics/EvalCtx.re
+++ b/src/haz3lcore/dynamics/EvalCtx.re
@@ -23,6 +23,8 @@ type cls =
   | BinFloatOp2
   | BinStringOp1
   | BinStringOp2
+  | BinPropOp1
+  | BinPropOp2
   | IfThenElse1
   | IfThenElse2
   | IfThenElse3
@@ -71,6 +73,8 @@ type t =
   | BinFloatOp2(TermBase.UExp.op_bin_float, DHExp.t, t)
   | BinStringOp1(TermBase.UExp.op_bin_string, t, DHExp.t)
   | BinStringOp2(TermBase.UExp.op_bin_string, DHExp.t, t)
+  | BinPropOp1(TermBase.UExp.op_bin_prop, t, DHExp.t)
+  | BinPropOp2(TermBase.UExp.op_bin_prop, DHExp.t, t)
   | Tuple(t, (list(DHExp.t), list(DHExp.t)))
   | ApBuiltin(string, t)
   | Test(KeywordID.t, t)
@@ -139,6 +143,8 @@ let rec fuzzy_mark =
   | BinFloatOp2(_)
   | BinStringOp1(_)
   | BinStringOp2(_)
+  | BinPropOp1(_)
+  | BinPropOp2(_)
   | Tuple(_)
   | ApBuiltin(_)
   | ListLit(_)
diff --git a/src/haz3lcore/dynamics/EvaluatorError.re b/src/haz3lcore/dynamics/EvaluatorError.re
index 7cd750d1bc..e0420ecceb 100644
--- a/src/haz3lcore/dynamics/EvaluatorError.re
+++ b/src/haz3lcore/dynamics/EvaluatorError.re
@@ -13,6 +13,7 @@ type t =
   | InvalidBoxedFloatLit(DHExp.t)
   | InvalidBoxedListLit(DHExp.t)
   | InvalidBoxedStringLit(DHExp.t)
+  | InvalidBoxedPropLit(DHExp.t)
   | InvalidBoxedTuple(DHExp.t)
   | InvalidBuiltin(string)
   | BadBuiltinAp(string, list(DHExp.t))
diff --git a/src/haz3lcore/dynamics/EvaluatorError.rei b/src/haz3lcore/dynamics/EvaluatorError.rei
index e5a07fe847..baf1f3c71c 100644
--- a/src/haz3lcore/dynamics/EvaluatorError.rei
+++ b/src/haz3lcore/dynamics/EvaluatorError.rei
@@ -11,6 +11,7 @@ type t =
   | InvalidBoxedFloatLit(DHExp.t)
   | InvalidBoxedListLit(DHExp.t)
   | InvalidBoxedStringLit(DHExp.t)
+  | InvalidBoxedPropLit(DHExp.t)
   | InvalidBoxedTuple(DHExp.t)
   | InvalidBuiltin(string)
   | BadBuiltinAp(string, list(DHExp.t))
diff --git a/src/haz3lcore/dynamics/EvaluatorPost.re b/src/haz3lcore/dynamics/EvaluatorPost.re
index 1d195a7481..9f63b83540 100644
--- a/src/haz3lcore/dynamics/EvaluatorPost.re
+++ b/src/haz3lcore/dynamics/EvaluatorPost.re
@@ -47,6 +47,7 @@ let rec pp_eval = (d: DHExp.t): m(DHExp.t) =>
   | FloatLit(_)
   | StringLit(_)
   | PropLit(_)
+  | JudgementLit(_)
   | Constructor(_) => d |> return
 
   | Sequence(d1, d2) =>
@@ -89,6 +90,11 @@ let rec pp_eval = (d: DHExp.t): m(DHExp.t) =>
     let* d2' = pp_eval(d2);
     BinStringOp(op, d1', d2') |> return;
 
+  | BinPropOp(op, d1, d2) =>
+    let* d1' = pp_eval(d1);
+    let* d2' = pp_eval(d2);
+    BinPropOp(op, d1', d2') |> return;
+
   | Cons(d1, d2) =>
     let* d1' = pp_eval(d1);
     let* d2' = pp_eval(d2);
@@ -273,6 +279,7 @@ and pp_uneval = (env: ClosureEnvironment.t, d: DHExp.t): m(DHExp.t) =>
   | FloatLit(_)
   | StringLit(_)
   | PropLit(_)
+  | JudgementLit(_)
   | Constructor(_) => d |> return
 
   | Test(id, d1) =>
@@ -329,6 +336,11 @@ and pp_uneval = (env: ClosureEnvironment.t, d: DHExp.t): m(DHExp.t) =>
     let* d2' = pp_uneval(env, d2);
     BinStringOp(op, d1', d2') |> return;
 
+  | BinPropOp(op, d1, d2) =>
+    let* d1' = pp_uneval(env, d1);
+    let* d2' = pp_uneval(env, d2);
+    BinPropOp(op, d1', d2') |> return;
+
   | IfThenElse(consistent, c, d1, d2) =>
     let* c' = pp_uneval(env, c);
     let* d1' = pp_uneval(env, d1);
@@ -461,6 +473,7 @@ let rec track_children_of_hole =
   | FloatLit(_)
   | StringLit(_)
   | PropLit(_)
+  | JudgementLit(_)
   | BuiltinFun(_)
   | BoundVar(_) => hii
   | Test(_, d)
@@ -477,6 +490,7 @@ let rec track_children_of_hole =
   | BinIntOp(_, d1, d2)
   | BinFloatOp(_, d1, d2)
   | BinStringOp(_, d1, d2)
+  | BinPropOp(_, d1, d2)
   | Cons(d1, d2) =>
     let hii = track_children_of_hole(hii, parent, d1);
     track_children_of_hole(hii, parent, d2);
diff --git a/src/haz3lcore/dynamics/EvaluatorStep.re b/src/haz3lcore/dynamics/EvaluatorStep.re
index b6fad324f2..b0a401b3ac 100644
--- a/src/haz3lcore/dynamics/EvaluatorStep.re
+++ b/src/haz3lcore/dynamics/EvaluatorStep.re
@@ -273,6 +273,12 @@ let rec compose = (ctx: EvalCtx.t, d: DHExp.t): DHExp.t => {
     | BinStringOp2(op, d1, ctx) =>
       let d2 = compose(ctx, d);
       BinStringOp(op, d1, d2);
+    | BinPropOp1(op, ctx, d2) =>
+      let d1 = compose(ctx, d);
+      BinPropOp(op, d1, d2);
+    | BinPropOp2(op, d1, ctx) =>
+      let d2 = compose(ctx, d);
+      BinPropOp(op, d1, d2);
     | Cons1(ctx, d2) =>
       let d1 = compose(ctx, d);
       Cons(d1, d2);
diff --git a/src/haz3lcore/dynamics/FilterMatcher.re b/src/haz3lcore/dynamics/FilterMatcher.re
index 27ee5d3a90..e22dc94ed2 100644
--- a/src/haz3lcore/dynamics/FilterMatcher.re
+++ b/src/haz3lcore/dynamics/FilterMatcher.re
@@ -78,6 +78,9 @@ let rec matches_exp =
   | (PropLit(dv), PropLit(fv)) => Derivation.Prop.eq(dv, fv)
   | (PropLit(_), _) => false
 
+  | (JudgementLit(dv), JudgementLit(fv)) => Derivation.Judgement.eq(dv, fv)
+  | (JudgementLit(_), _) => false
+
   | (Constructor(_), Ap(Constructor("~MVal"), Tuple([]))) => true
   | (Constructor(dt), Constructor(ft)) => dt == ft
   | (Constructor(_), _) => false
@@ -169,6 +172,12 @@ let rec matches_exp =
     && matches_exp(env, d2, f2)
   | (BinStringOp(_), _) => false
 
+  | (BinPropOp(d_op_bin, d1, d2), BinPropOp(f_op_bin, f1, f2)) =>
+    d_op_bin == f_op_bin
+    && matches_exp(env, d1, f1)
+    && matches_exp(env, d2, f2)
+  | (BinPropOp(_), _) => false
+
   | (ListConcat(_), _) => false
 
   | (
diff --git a/src/haz3lcore/dynamics/PatternMatch.re b/src/haz3lcore/dynamics/PatternMatch.re
index 4f84c806cf..c3aecdd5a1 100644
--- a/src/haz3lcore/dynamics/PatternMatch.re
+++ b/src/haz3lcore/dynamics/PatternMatch.re
@@ -246,6 +246,7 @@ and matches_cast_Sum =
   | BinIntOp(_)
   | BinFloatOp(_)
   | BinStringOp(_)
+  | BinPropOp(_)
   | InconsistentBranches(_)
   | EmptyHole(_)
   | NonEmptyHole(_)
@@ -265,6 +266,7 @@ and matches_cast_Sum =
   | FloatLit(_)
   | StringLit(_)
   | PropLit(_)
+  | JudgementLit(_)
   | ListLit(_)
   | Tuple(_)
   | Sequence(_, _)
@@ -345,6 +347,7 @@ and matches_cast_Tuple =
   | BinIntOp(_, _, _)
   | BinFloatOp(_, _, _)
   | BinStringOp(_)
+  | BinPropOp(_)
   | BoolLit(_) => DoesNotMatch
   | IntLit(_) => DoesNotMatch
   | Sequence(_)
@@ -353,6 +356,7 @@ and matches_cast_Tuple =
   | FloatLit(_) => DoesNotMatch
   | StringLit(_) => DoesNotMatch
   | PropLit(_) => DoesNotMatch
+  | JudgementLit(_) => DoesNotMatch
   | ListLit(_) => DoesNotMatch
   | Cons(_, _) => DoesNotMatch
   | ListConcat(_) => DoesNotMatch
@@ -485,6 +489,7 @@ and matches_cast_Cons =
   | BinIntOp(_, _, _)
   | BinFloatOp(_, _, _)
   | BinStringOp(_)
+  | BinPropOp(_)
   | ListConcat(_)
   | BuiltinFun(_) => DoesNotMatch
   | BoolLit(_) => DoesNotMatch
@@ -494,6 +499,7 @@ and matches_cast_Cons =
   | FloatLit(_) => DoesNotMatch
   | StringLit(_) => DoesNotMatch
   | PropLit(_) => DoesNotMatch
+  | JudgementLit(_) => DoesNotMatch
   | Tuple(_) => DoesNotMatch
   | Prj(_) => IndetMatch
   | Constructor(_) => DoesNotMatch
diff --git a/src/haz3lcore/dynamics/Stepper.re b/src/haz3lcore/dynamics/Stepper.re
index 0e9f0e478a..6249333855 100644
--- a/src/haz3lcore/dynamics/Stepper.re
+++ b/src/haz3lcore/dynamics/Stepper.re
@@ -122,6 +122,12 @@ let rec matches =
     | BinStringOp2(op, d1, ctx) =>
       let+ ctx = matches(env, flt, ctx, exp, act, idx);
       BinStringOp2(op, d1, ctx);
+    | BinPropOp1(op, ctx, d2) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      BinPropOp1(op, ctx, d2);
+    | BinPropOp2(op, d1, ctx) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      BinPropOp2(op, d1, ctx);
     | Tuple(ctx, ds) =>
       let+ ctx = matches(env, flt, ctx, exp, act, idx);
       Tuple(ctx, ds);
@@ -402,6 +408,7 @@ let get_justification: step_kind => string =
   | BinFloatOp(Equals | NotEquals)
   | BinStringOp(Equals) => "check equality"
   | BinStringOp(Concat) => "string manipulation"
+  | BinPropOp(_) => "propositional logic"
   | BinBoolOp(_) => "boolean logic"
   | Conditional(_) => "conditional"
   | ListCons => "list manipulation"
diff --git a/src/haz3lcore/dynamics/Substitution.re b/src/haz3lcore/dynamics/Substitution.re
index f264a07ac9..ed2c942165 100644
--- a/src/haz3lcore/dynamics/Substitution.re
+++ b/src/haz3lcore/dynamics/Substitution.re
@@ -62,6 +62,7 @@ let rec subst_var = (d1: DHExp.t, x: Var.t, d2: DHExp.t): DHExp.t =>
   | FloatLit(_)
   | StringLit(_)
   | PropLit(_)
+  | JudgementLit(_)
   | Constructor(_) => d2
   | ListLit(a, b, c, ds) =>
     ListLit(a, b, c, List.map(subst_var(d1, x), ds))
@@ -91,6 +92,10 @@ let rec subst_var = (d1: DHExp.t, x: Var.t, d2: DHExp.t): DHExp.t =>
     let d3 = subst_var(d1, x, d3);
     let d4 = subst_var(d1, x, d4);
     BinStringOp(op, d3, d4);
+  | BinPropOp(op, d3, d4) =>
+    let d3 = subst_var(d1, x, d3);
+    let d4 = subst_var(d1, x, d4);
+    BinPropOp(op, d3, d4);
   | ConsistentCase(Case(d3, rules, n)) =>
     let d3 = subst_var(d1, x, d3);
     let rules = subst_var_rules(d1, x, rules);
diff --git a/src/haz3lcore/dynamics/Transition.re b/src/haz3lcore/dynamics/Transition.re
index 1b10c8ebe0..929d8b1648 100644
--- a/src/haz3lcore/dynamics/Transition.re
+++ b/src/haz3lcore/dynamics/Transition.re
@@ -62,6 +62,7 @@ type step_kind =
   | BinIntOp(TermBase.UExp.op_bin_int)
   | BinFloatOp(TermBase.UExp.op_bin_float)
   | BinStringOp(TermBase.UExp.op_bin_string)
+  | BinPropOp(TermBase.UExp.op_bin_prop)
   | Conditional(bool)
   | Projection
   | ListCons
@@ -107,6 +108,7 @@ module CastHelpers = {
     | Float
     | String
     | Prop
+    | Judgement
     | Var(_)
     | Rec(_)
     | Arrow(Unknown(_), Unknown(_))
@@ -323,6 +325,7 @@ module Transition = (EV: EV_MODE) => {
     | FloatLit(_)
     | StringLit(_)
     | PropLit(_)
+    | JudgementLit(_)
     | Constructor(_)
     | BuiltinFun(_) =>
       let. _ = otherwise(env, d);
@@ -476,6 +479,28 @@ module Transition = (EV: EV_MODE) => {
         kind: BinStringOp(op),
         value: true,
       });
+    | BinPropOp(op, d1, d2) =>
+      let. _ = otherwise(env, (d1, d2) => BinPropOp(op, d1, d2))
+      and. d1' =
+        req_value(req(state, env), d1 => BinPropOp1(op, d1, d2), d1)
+      and. d2' =
+        req_value(req(state, env), d2 => BinPropOp2(op, d1, d2), d2);
+      Step({
+        apply: () =>
+          switch (d1', d2') {
+          | (PropLit(p1), PropLit(p2)) =>
+            switch (op) {
+            | And => PropLit(And(p1, p2))
+            | Or => PropLit(Or(p1, p2))
+            | Implies => PropLit(Implies(p1, p2))
+            }
+          | (PropLit(_), _) =>
+            raise(EvaluatorError.Exception(InvalidBoxedPropLit(d2')))
+          | _ => raise(EvaluatorError.Exception(InvalidBoxedPropLit(d1')))
+          },
+        kind: BinPropOp(op),
+        value: true,
+      });
     | Tuple(ds) =>
       let. _ = otherwise(env, ds => Tuple(ds))
       and. _ =
@@ -663,6 +688,7 @@ let should_hide_step = (~settings: CoreSettings.Evaluation.t) =>
   | BinIntOp(_)
   | BinFloatOp(_)
   | BinStringOp(_)
+  | BinPropOp(_)
   | ListCons
   | ListConcat
   | CaseApply
diff --git a/src/haz3lcore/lang/Form.re b/src/haz3lcore/lang/Form.re
index e726409bb7..54b3d862ed 100644
--- a/src/haz3lcore/lang/Form.re
+++ b/src/haz3lcore/lang/Form.re
@@ -256,6 +256,10 @@ let forms: list((string, t)) = [
   ("equals", mk_infix("==", Exp, P.eqs)),
   ("string_equals", mk_infix("$==", Exp, P.eqs)),
   ("string_concat", mk_infix("++", Exp, P.plus)),
+  ("prop_and", mk_infix("/\\", Exp, P.prop_and)),
+  ("prop_or", mk_infix("\\/", Exp, P.prop_or)),
+  ("prop_implies", mk_infix("==>", Exp, P.prop_implies)),
+  ("judgement_entail", mk_infix("|-", Exp, P.judgement_entail)),
   ("lt", mk_infix("<", Exp, P.eqs)),
   ("gt", mk_infix(">", Exp, P.eqs)),
   ("not_equals", mk_infix("!=", Exp, P.eqs)),
diff --git a/src/haz3lcore/lang/Precedence.re b/src/haz3lcore/lang/Precedence.re
index b7d00796a5..0e00377c08 100644
--- a/src/haz3lcore/lang/Precedence.re
+++ b/src/haz3lcore/lang/Precedence.re
@@ -23,16 +23,19 @@ let or_ = 11;
 let ann = 12;
 let if_ = 13;
 let fun_ = 14;
-let prod = 15;
-let semi = 16;
-let let_ = 17;
-let filter = 18;
-let rule_arr = 19;
-let rule_pre = 20;
-let rule_sep = 21;
-let case_ = 22;
-
-let min = 23;
+let prop_and = 15;
+let prop_or = 16;
+let prop_implies = 17;
+let judgement_entail = 18;
+let prod = 19;
+let semi = 20;
+let let_ = 21;
+let filter = 22;
+let rule_arr = 23;
+let rule_pre = 24;
+let rule_sep = 25;
+let case_ = 26;
+let min = 27;
 
 let compare = (p1: t, p2: t): int =>
   (-1) * Int.compare((p1 :> int), (p2 :> int));
diff --git a/src/haz3lcore/statics/Derivation.re b/src/haz3lcore/statics/Derivation.re
index c85a9e3709..2575f9b112 100644
--- a/src/haz3lcore/statics/Derivation.re
+++ b/src/haz3lcore/statics/Derivation.re
@@ -35,3 +35,37 @@ module rec Prop: {
     | Truth => "⊤"
     | Falsity => "⊥";
 };
+
+module Ctx: {
+  [@deriving (show({with_path: false}), sexp, yojson)]
+  type t = list(Prop.t);
+  let repr: t => string;
+  let eq: (t, t) => bool;
+  let extend: (t, Prop.t) => t;
+} = {
+  [@deriving (show({with_path: false}), sexp, yojson)]
+  type t = list(Prop.t);
+  let repr = ctx => ctx |> List.map(Prop.repr) |> String.concat(", ");
+  let eq = (a, b) => a == b;
+  let extend = (ctx, prop) =>
+    if (ctx |> List.mem(prop)) {
+      ctx;
+    } else {
+      ctx @ [prop];
+    };
+};
+
+module Judgement: {
+  [@deriving (show({with_path: false}), sexp, yojson)]
+  type t =
+    | Entail(Ctx.t, Prop.t);
+  let repr: t => string;
+  let eq: (t, t) => bool;
+} = {
+  [@deriving (show({with_path: false}), sexp, yojson)]
+  type t =
+    | Entail(Ctx.t, Prop.t);
+  let repr = (Entail(ctx, prop)) =>
+    Printf.sprintf("%s ⊢ %s", Ctx.repr(ctx), Prop.repr(prop));
+  let eq = (a, b) => a == b;
+};
diff --git a/src/haz3lcore/statics/MakeTerm.re b/src/haz3lcore/statics/MakeTerm.re
index a26a22a6ea..eae967516b 100644
--- a/src/haz3lcore/statics/MakeTerm.re
+++ b/src/haz3lcore/statics/MakeTerm.re
@@ -269,6 +269,9 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = {
           | ([";"], []) => Seq(l, r)
           | (["++"], []) => BinOp(String(Concat), l, r)
           | (["$=="], []) => BinOp(String(Equals), l, r)
+          | (["/\\"], []) => BinOp(Prop(And), l, r)
+          | (["\\/"], []) => BinOp(Prop(Or), l, r)
+          | (["==>"], []) => BinOp(Prop(Implies), l, r)
           | (["|>"], []) => Pipeline(l, r)
           | (["@"], []) => ListConcat(l, r)
           | _ => hole(tm)
@@ -367,6 +370,7 @@ and typ_term: unsorted => (UTyp.term, list(Id.t)) = {
         | (["Float"], []) => Float
         | (["String"], []) => String
         | (["Prop"], []) => Prop
+        | (["Judgement"], []) => Judgement
         | ([t], []) when Form.is_typ_var(t) => Var(t)
         | (["(", ")"], [Typ(body)]) => Parens(body)
         | (["[", "]"], [Typ(body)]) => List(body)
diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re
index 2e35dc88ea..fd152cfb2b 100644
--- a/src/haz3lcore/statics/Statics.re
+++ b/src/haz3lcore/statics/Statics.re
@@ -108,12 +108,19 @@ let typ_exp_binop_bin_string: UExp.op_bin_string => Typ.t =
   | Concat => String
   | Equals => Bool;
 
+let typ_exp_binop_bin_prop: UExp.op_bin_prop => Typ.t =
+  fun
+  | And
+  | Or
+  | Implies => Prop;
+
 let typ_exp_binop: UExp.op_bin => (Typ.t, Typ.t, Typ.t) =
   fun
   | Bool(And | Or) => (Bool, Bool, Bool)
   | Int(op) => (Int, Int, typ_exp_binop_bin_int(op))
   | Float(op) => (Float, Float, typ_exp_binop_bin_float(op))
-  | String(op) => (String, String, typ_exp_binop_bin_string(op));
+  | String(op) => (String, String, typ_exp_binop_bin_string(op))
+  | Prop(op) => (Prop, Prop, typ_exp_binop_bin_prop(op));
 
 let typ_exp_unop: UExp.op_un => (Typ.t, Typ.t) =
   fun
@@ -219,6 +226,7 @@ and uexp_to_info_map =
   | Float(_) => atomic(Just(Float))
   | String(_) => atomic(Just(String))
   | Prop(_) => atomic(Just(Prop))
+  | Judgement(_) => atomic(Just(Judgement))
   | ListLit(es) =>
     let ids = List.map(UExp.rep_id, es);
     let modes = Mode.of_list_lit(ctx, List.length(es), mode);
@@ -608,6 +616,7 @@ and utyp_to_info_map =
   | Float
   | Bool
   | Prop
+  | Judgement
   | String => add(m)
   | Var(_)
   | Constructor(_) =>
diff --git a/src/haz3lcore/statics/Term.re b/src/haz3lcore/statics/Term.re
index 5976cfab6d..a1a1ccaa78 100644
--- a/src/haz3lcore/statics/Term.re
+++ b/src/haz3lcore/statics/Term.re
@@ -30,6 +30,7 @@ module UTyp = {
     | Bool
     | String
     | Prop
+    | Judgement
     | Arrow
     | Tuple
     | Sum
@@ -62,6 +63,7 @@ module UTyp = {
     | Bool => Bool
     | String => String
     | Prop => Prop
+    | Judgement => Judgement
     | List(_) => List
     | Arrow(_) => Arrow
     | Var(_) => Var
@@ -80,6 +82,7 @@ module UTyp = {
     | Float
     | String
     | Prop
+    | Judgement
     | Bool => "Base type"
     | Var => "Type variable"
     | Constructor => "Sum constructor"
@@ -102,6 +105,7 @@ module UTyp = {
       | Float => Float
       | String => String
       | Prop => Prop
+      | Judgement => Judgement
       | Var(name) =>
         switch (Ctx.lookup_tvar(ctx, name)) {
         | Some(_) => Var(name)
@@ -390,6 +394,7 @@ module UExp = {
     | Float
     | String
     | Prop
+    | Judgement
     | ListLit
     | Constructor
     | Fun
@@ -435,6 +440,8 @@ module UExp = {
     | Float(_) => Float
     | String(_) => String
     | Prop(_) => Prop
+
+    | Judgement(_) => Judgement
     | ListLit(_) => ListLit
     | Constructor(_) => Constructor
     | Fun(_) => Fun
@@ -512,12 +519,19 @@ module UExp = {
     | Concat => "String Concatenation"
     | Equals => "String Equality";
 
+  let show_op_bin_prop: op_bin_prop => string =
+    fun
+    | And => "Propositional Conjunction"
+    | Or => "Propositional Disjunction"
+    | Implies => "Propositional Implication";
+
   let show_binop: op_bin => string =
     fun
     | Int(op) => show_op_bin_int(op)
     | Float(op) => show_op_bin_float(op)
     | Bool(op) => show_op_bin_bool(op)
-    | String(op) => show_op_bin_string(op);
+    | String(op) => show_op_bin_string(op)
+    | Prop(op) => show_op_bin_prop(op);
 
   let show_cls: cls => string =
     fun
@@ -531,6 +545,7 @@ module UExp = {
     | Float => "Float literal"
     | String => "String literal"
     | Prop => "Proposition"
+    | Judgement => "Judgement"
     | ListLit => "List literal"
     | Constructor => "Constructor"
     | Fun => "Function literal"
@@ -567,6 +582,7 @@ module UExp = {
     | Float(_)
     | String(_)
     | Prop(_)
+    | Judgement(_)
     | ListLit(_)
     | Tuple(_)
     | Var(_)
@@ -604,6 +620,7 @@ module UExp = {
       | Float(_)
       | String(_)
       | Prop(_)
+      | Judgement(_)
       | ListLit(_)
       | Fun(_)
       | Var(_)
@@ -655,6 +672,7 @@ module UExp = {
       | Float(_)
       | String(_)
       | Prop(_)
+      | Judgement(_)
       | ListLit(_)
       | Fun(_)
       | Var(_)
diff --git a/src/haz3lcore/statics/TermBase.re b/src/haz3lcore/statics/TermBase.re
index bf6e477f91..c7e38b8623 100644
--- a/src/haz3lcore/statics/TermBase.re
+++ b/src/haz3lcore/statics/TermBase.re
@@ -89,6 +89,12 @@ and UExp: {
     | Concat
     | Equals;
 
+  [@deriving (show({with_path: false}), sexp, yojson)]
+  type op_bin_prop =
+    | And
+    | Or
+    | Implies;
+
   [@deriving (show({with_path: false}), sexp, yojson)]
   type op_un =
     | Meta(op_un_meta)
@@ -100,7 +106,8 @@ and UExp: {
     | Int(op_bin_int)
     | Float(op_bin_float)
     | Bool(op_bin_bool)
-    | String(op_bin_string);
+    | String(op_bin_string)
+    | Prop(op_bin_prop);
 
   [@deriving (show({with_path: false}), sexp, yojson)]
   type cls =
@@ -113,6 +120,7 @@ and UExp: {
     | Float
     | String
     | Prop
+    | Judgement
     | ListLit
     | Tag
     | Fun
@@ -148,6 +156,7 @@ and UExp: {
     | Float(float)
     | String(string)
     | Prop(Derivation.Prop.t)
+    | Judgement(Derivation.Judgement.t)
     | ListLit(list(t))
     | Constructor(string)
     | Fun(UPat.t, t)
@@ -178,6 +187,7 @@ and UExp: {
   let int_op_to_string: op_bin_int => string;
   let float_op_to_string: op_bin_float => string;
   let string_op_to_string: op_bin_string => string;
+  let prop_op_to_string: op_bin_prop => string;
 } = {
   [@deriving (show({with_path: false}), sexp, yojson)]
   type op_un_bool =
@@ -229,6 +239,12 @@ and UExp: {
     | Concat
     | Equals;
 
+  [@deriving (show({with_path: false}), sexp, yojson)]
+  type op_bin_prop =
+    | And
+    | Or
+    | Implies;
+
   [@deriving (show({with_path: false}), sexp, yojson)]
   type op_un =
     | Meta(op_un_meta)
@@ -240,7 +256,8 @@ and UExp: {
     | Int(op_bin_int)
     | Float(op_bin_float)
     | Bool(op_bin_bool)
-    | String(op_bin_string);
+    | String(op_bin_string)
+    | Prop(op_bin_prop);
 
   [@deriving (show({with_path: false}), sexp, yojson)]
   type cls =
@@ -253,6 +270,7 @@ and UExp: {
     | Float
     | String
     | Prop
+    | Judgement
     | ListLit
     | Tag
     | Fun
@@ -288,6 +306,7 @@ and UExp: {
     | Float(float)
     | String(string)
     | Prop(Derivation.Prop.t)
+    | Judgement(Derivation.Judgement.t)
     | ListLit(list(t))
     | Constructor(string)
     | Fun(UPat.t, t)
@@ -359,6 +378,14 @@ and UExp: {
     | Equals => "$=="
     };
   };
+
+  let prop_op_to_string = (op: op_bin_prop): string => {
+    switch (op) {
+    | And => "/\\"
+    | Or => "\\/"
+    | Implies => "==>"
+    };
+  };
 }
 and UPat: {
   [@deriving (show({with_path: false}), sexp, yojson)]
@@ -420,6 +447,7 @@ and UTyp: {
     | Bool
     | String
     | Prop
+    | Judgement
     | List(t)
     | Var(string)
     | Constructor(string)
@@ -446,6 +474,7 @@ and UTyp: {
     | Bool
     | String
     | Prop
+    | Judgement
     | List(t)
     | Var(string)
     | Constructor(string)
diff --git a/src/haz3lcore/statics/TypBase.re b/src/haz3lcore/statics/TypBase.re
index 97a4f60822..6f334a65a8 100644
--- a/src/haz3lcore/statics/TypBase.re
+++ b/src/haz3lcore/statics/TypBase.re
@@ -28,6 +28,7 @@ module rec Typ: {
     | Bool
     | String
     | Prop
+    | Judgement
     | Var(TypVar.t)
     | List(t)
     | Arrow(t, t)
@@ -87,6 +88,7 @@ module rec Typ: {
     | Bool
     | String
     | Prop
+    | Judgement
     | Var(TypVar.t)
     | List(t)
     | Arrow(t, t)
@@ -131,6 +133,7 @@ module rec Typ: {
     | Bool
     | String
     | Prop
+    | Judgement
     | Unknown(_)
     | Var(_)
     | Rec(_)
@@ -147,6 +150,7 @@ module rec Typ: {
     | Bool => Bool
     | String => String
     | Prop => Prop
+    | Judgement => Judgement
     | Unknown(prov) => Unknown(prov)
     | Arrow(ty1, ty2) => Arrow(subst(s, x, ty1), subst(s, x, ty2))
     | Prod(tys) => Prod(List.map(subst(s, x), tys))
@@ -180,6 +184,8 @@ module rec Typ: {
     | (String, _) => false
     | (Prop, Prop) => true
     | (Prop, _) => false
+    | (Judgement, Judgement) => true
+    | (Judgement, _) => false
     | (Unknown(_), Unknown(_)) => true
     | (Unknown(_), _) => false
     | (Arrow(t1, t2), Arrow(t1', t2')) => eq(t1, t1') && eq(t2, t2')
@@ -204,6 +210,7 @@ module rec Typ: {
     | Bool
     | String => []
     | Prop => []
+    | Judgement => []
     | Var(v) => List.mem(v, bound) ? [] : [v]
     | List(ty) => free_vars(~bound, ty)
     | Arrow(t1, t2) => free_vars(~bound, t1) @ free_vars(~bound, t2)
@@ -274,6 +281,8 @@ module rec Typ: {
     | (String, _) => None
     | (Prop, Prop) => Some(Prop)
     | (Prop, _) => None
+    | (Judgement, Judgement) => Some(Judgement)
+    | (Judgement, _) => None
     | (Arrow(ty1, ty2), Arrow(ty1', ty2')) =>
       let* ty1 = join'(ty1, ty1');
       let+ ty2 = join'(ty2, ty2');
@@ -357,6 +366,7 @@ module rec Typ: {
     | Bool
     | String => ty
     | Prop => Prop
+    | Judgement => Judgement
     | List(t) => List(normalize(ctx, t))
     | Arrow(t1, t2) => Arrow(normalize(ctx, t1), normalize(ctx, t2))
     | Prod(ts) => Prod(List.map(normalize(ctx), ts))
diff --git a/src/haz3lcore/zipper/EditorUtil.re b/src/haz3lcore/zipper/EditorUtil.re
index 752d1bb54e..457fe0c8b4 100644
--- a/src/haz3lcore/zipper/EditorUtil.re
+++ b/src/haz3lcore/zipper/EditorUtil.re
@@ -53,6 +53,7 @@ let rec append_exp = (e1: TermBase.UExp.t, e2: TermBase.UExp.t) => {
   | Float(_)
   | String(_)
   | Prop(_)
+  | Judgement(_)
   | ListLit(_)
   | Constructor(_)
   | Fun(_)
diff --git a/src/haz3lschool/SyntaxTest.re b/src/haz3lschool/SyntaxTest.re
index 775b8499a7..bdfb63411b 100644
--- a/src/haz3lschool/SyntaxTest.re
+++ b/src/haz3lschool/SyntaxTest.re
@@ -107,6 +107,7 @@ let rec find_fn =
   | Float(_)
   | String(_)
   | Prop(_)
+  | Judgement(_)
   | Constructor(_)
   | Var(_) => l
   };
@@ -159,6 +160,7 @@ let rec var_mention = (name: string, uexp: Term.UExp.t): bool => {
   | Float(_)
   | String(_)
   | Prop(_)
+  | Judgement(_)
   | Constructor(_)
   | Deferral(_) => false
   | Fun(args, body) =>
@@ -213,6 +215,7 @@ let rec var_applied = (name: string, uexp: Term.UExp.t): bool => {
   | Float(_)
   | String(_)
   | Prop(_)
+  | Judgement(_)
   | Constructor(_)
   | Deferral(_) => false
   | Fun(args, body) =>
@@ -295,6 +298,7 @@ let rec tail_check = (name: string, uexp: Term.UExp.t): bool => {
   | Float(_)
   | String(_)
   | Prop(_)
+  | Judgement(_)
   | Constructor(_)
   | Var(_) => true
   | Fun(args, body) =>
diff --git a/src/haz3lweb/explainthis/Example.re b/src/haz3lweb/explainthis/Example.re
index 217ed04f40..298f3450ae 100644
--- a/src/haz3lweb/explainthis/Example.re
+++ b/src/haz3lweb/explainthis/Example.re
@@ -104,6 +104,9 @@ let fgt = () => mk_monotile(Form.get("fgt"));
 let fgte = () => mk_monotile(Form.get("fgte"));
 let sequals = () => mk_monotile(Form.get("string_equals"));
 let sconcat = () => mk_monotile(Form.get("string_concat"));
+let prop_and = () => mk_monotile(Form.get("prop_and"));
+let prop_or = () => mk_monotile(Form.get("prop_or"));
+let prop_implies = () => mk_monotile(Form.get("prop_implies"));
 let logical_and = () => mk_monotile(Form.get("logical_and"));
 let logical_or = () => mk_monotile(Form.get("logical_or"));
 let comma_exp = () => mk_monotile(Form.get("comma_exp"));
diff --git a/src/haz3lweb/explainthis/ExplainThisForm.re b/src/haz3lweb/explainthis/ExplainThisForm.re
index 57205771b3..df5b187459 100644
--- a/src/haz3lweb/explainthis/ExplainThisForm.re
+++ b/src/haz3lweb/explainthis/ExplainThisForm.re
@@ -146,6 +146,7 @@ type form_id =
   | FloatExp
   | StringExp
   | PropExp
+  | JudgementExp
   | VarExp
   | CtrExp
   | ListExp
@@ -192,6 +193,7 @@ type form_id =
   | BoolTyp
   | StrTyp
   | PropTyp
+  | JudgementTyp
   | VarTyp
   | ListTyp
   | ArrowTyp
@@ -235,6 +237,7 @@ type group_id =
   | FloatExp
   | StringExp
   | PropExp
+  | JudgementExp
   | VarExp
   | CtrExp
   | ListExp
@@ -282,6 +285,7 @@ type group_id =
   | BoolTyp
   | StrTyp
   | PropTyp
+  | JudgementTyp
   | VarTyp
   | ListTyp
   | ArrowTyp
diff --git a/src/haz3lweb/explainthis/data/OpExp.re b/src/haz3lweb/explainthis/data/OpExp.re
index 04e3be4fcd..cf1b7b44e9 100644
--- a/src/haz3lweb/explainthis/data/OpExp.re
+++ b/src/haz3lweb/explainthis/data/OpExp.re
@@ -760,6 +760,63 @@ let str_concat_exp: form = {
   };
 };
 
+let prop_and_exp_coloring_ids =
+    (~left_id: Id.t, ~right_id: Id.t): list((Id.t, Id.t)) =>
+  _binop_exp_coloring_ids(
+    Piece.id(_exp1),
+    Piece.id(_exp2),
+    ~left_id,
+    ~right_id,
+  );
+let prop_and_exp: form = {
+  let explanation = "Returns the logical conjunction of the [*left operand*](%s) and the [*right operand*](%s).";
+  {
+    id: BinOpExp(Prop(And)),
+    syntactic_form: [_exp1, space(), prop_and(), space(), _exp2],
+    expandable_id: None,
+    explanation,
+    examples: [],
+  };
+};
+
+let prop_or_exp_coloring_ids =
+    (~left_id: Id.t, ~right_id: Id.t): list((Id.t, Id.t)) =>
+  _binop_exp_coloring_ids(
+    Piece.id(_exp1),
+    Piece.id(_exp2),
+    ~left_id,
+    ~right_id,
+  );
+let prop_or_exp: form = {
+  let explanation = "Returns the logical disjunction of the [*left operand*](%s) and the [*right operand*](%s).";
+  {
+    id: BinOpExp(Prop(Or)),
+    syntactic_form: [_exp1, space(), prop_or(), space(), _exp2],
+    expandable_id: None,
+    explanation,
+    examples: [],
+  };
+};
+
+let prop_implies_exp_coloring_ids =
+    (~left_id: Id.t, ~right_id: Id.t): list((Id.t, Id.t)) =>
+  _binop_exp_coloring_ids(
+    Piece.id(_exp1),
+    Piece.id(_exp2),
+    ~left_id,
+    ~right_id,
+  );
+let prop_implies_exp: form = {
+  let explanation = "Returns the logical implication of the [*left operand*](%s) and the [*right operand*](%s).";
+  {
+    id: BinOpExp(Prop(Implies)),
+    syntactic_form: [_exp1, space(), prop_implies(), space(), _exp2],
+    expandable_id: None,
+    explanation,
+    examples: [],
+  };
+};
+
 let bool_un_not: group = {
   id: UnOpExp(Bool(Not)),
   forms: [bool_unary_not_exp],
@@ -878,3 +935,12 @@ let string_concat: group = {
   id: BinOpExp(String(Concat)),
   forms: [str_concat_exp],
 };
+
+let prop_and: group = {id: BinOpExp(Bool(And)), forms: [prop_and_exp]};
+
+let prop_or: group = {id: BinOpExp(Bool(Or)), forms: [prop_or_exp]};
+
+let prop_implies: group = {
+  id: UnOpExp(Bool(Not)),
+  forms: [prop_implies_exp],
+};
diff --git a/src/haz3lweb/explainthis/data/TerminalExp.re b/src/haz3lweb/explainthis/data/TerminalExp.re
index 43e45ebb89..c1654f9b6a 100644
--- a/src/haz3lweb/explainthis/data/TerminalExp.re
+++ b/src/haz3lweb/explainthis/data/TerminalExp.re
@@ -82,6 +82,18 @@ let prop_exps = (p: Derivation.Prop.t): group => {
   forms: [prop_exp(p)],
 };
 
+let judgement_exp = (j: Derivation.Judgement.t): form => {
+  id: JudgementExp,
+  syntactic_form: [j |> Derivation.Judgement.repr |> exp],
+  expandable_id: None,
+  explanation: "A judgement literal.",
+  examples: [],
+};
+let judgement_exps = (j: Derivation.Judgement.t): group => {
+  id: JudgementExp,
+  forms: [judgement_exp(j)],
+};
+
 let var_exp = (n: string): form => {
   id: VarExp,
   syntactic_form: [n |> abbreviate |> exp],
diff --git a/src/haz3lweb/explainthis/data/TerminalTyp.re b/src/haz3lweb/explainthis/data/TerminalTyp.re
index 134caaefc9..c7ec5def2b 100644
--- a/src/haz3lweb/explainthis/data/TerminalTyp.re
+++ b/src/haz3lweb/explainthis/data/TerminalTyp.re
@@ -56,6 +56,17 @@ let prop_typ: form = {
   };
 };
 
+let judgement_typ: form = {
+  let explanation = "The `Judgement` type classifies judgements.";
+  {
+    id: JudgementTyp,
+    syntactic_form: [typ("Judgement")],
+    expandable_id: None,
+    explanation,
+    examples: [],
+  };
+};
+
 let var_typ = (name: string): form => {
   let explanation = "`%s` is a type variable.";
   {
@@ -77,4 +88,6 @@ let str: group = {id: StrTyp, forms: [str_typ]};
 
 let prop: group = {id: PropTyp, forms: [prop_typ]};
 
+let judgement: group = {id: JudgementTyp, forms: [judgement_typ]};
+
 let var = (name: string): group => {id: VarTyp, forms: [var_typ(name)]};
diff --git a/src/haz3lweb/view/ExplainThis.re b/src/haz3lweb/view/ExplainThis.re
index cf8b5a28c7..d905f2aabd 100644
--- a/src/haz3lweb/view/ExplainThis.re
+++ b/src/haz3lweb/view/ExplainThis.re
@@ -548,6 +548,7 @@ let get_doc =
       | Float(f) => get_message(TerminalExp.float_exps(f))
       | String(s) => get_message(TerminalExp.string_exps(s))
       | Prop(p) => get_message(TerminalExp.prop_exps(p))
+      | Judgement(j) => get_message(TerminalExp.judgement_exps(j))
       | ListLit(terms) =>
         get_message(
           ~format=
@@ -1795,6 +1796,9 @@ let get_doc =
           | Bool(Or) => (bool_or, bool_or_exp_coloring_ids)
           | String(Equals) => (string_equal, str_eq_exp_coloring_ids)
           | String(Concat) => (string_concat, str_concat_exp_coloring_ids)
+          | Prop(And) => (prop_and, prop_and_exp_coloring_ids)
+          | Prop(Or) => (prop_or, prop_or_exp_coloring_ids)
+          | Prop(Implies) => (prop_implies, prop_implies_exp_coloring_ids)
           };
         let left_id = List.nth(left.ids, 0);
         let right_id = List.nth(right.ids, 0);
@@ -2067,6 +2071,7 @@ let get_doc =
     | Bool => get_message(TerminalTyp.bool)
     | String => get_message(TerminalTyp.str)
     | Prop => get_message(TerminalTyp.prop)
+    | Judgement => get_message(TerminalTyp.judgement)
     | List(elem) =>
       let elem_id = List.nth(elem.ids, 0);
       get_message(
diff --git a/src/haz3lweb/view/Type.re b/src/haz3lweb/view/Type.re
index 833ec9b9bd..d7e8343697 100644
--- a/src/haz3lweb/view/Type.re
+++ b/src/haz3lweb/view/Type.re
@@ -34,6 +34,7 @@ let rec view_ty = (ty: Haz3lcore.Typ.t): Node.t =>
   | String => ty_view("String", "String")
   | Bool => ty_view("Bool", "Bool")
   | Prop => ty_view("Prop", "Prop")
+  | Judgement => ty_view("Judgement", "Judgement")
   | Var(name) => ty_view("Var", name)
   | Rec(x, t) =>
     div(
diff --git a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re
index 9cdf2ecead..9cc1dc5ced 100644
--- a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re
+++ b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re
@@ -42,6 +42,12 @@ let precedence_bin_string_op = (bso: TermBase.UExp.op_bin_string) =>
   | Concat => DHDoc_common.precedence_Plus
   | Equals => DHDoc_common.precedence_Equals
   };
+let precedence_bin_prop_op = (bpo: TermBase.UExp.op_bin_prop) =>
+  switch (bpo) {
+  | And => DHDoc_common.precedence_PropAnd
+  | Or => DHDoc_common.precedence_PropOr
+  | Implies => DHDoc_common.precedence_PropImplies
+  };
 let rec precedence = (~show_casts: bool, d: DHExp.t) => {
   let precedence' = precedence(~show_casts);
   switch (d) {
@@ -56,6 +62,7 @@ let rec precedence = (~show_casts: bool, d: DHExp.t) => {
   | FloatLit(_)
   | StringLit(_)
   | PropLit(_)
+  | JudgementLit(_)
   | ListLit(_)
   | Prj(_)
   | EmptyHole(_)
@@ -83,6 +90,7 @@ let rec precedence = (~show_casts: bool, d: DHExp.t) => {
   | BinIntOp(op, _, _) => precedence_bin_int_op(op)
   | BinFloatOp(op, _, _) => precedence_bin_float_op(op)
   | BinStringOp(op, _, _) => precedence_bin_string_op(op)
+  | BinPropOp(op, _, _) => precedence_bin_prop_op(op)
 
   | NonEmptyHole(_, _, _, d) => precedence'(d)
   };
@@ -100,6 +108,9 @@ let mk_bin_float_op = (op: TermBase.UExp.op_bin_float): DHDoc.t =>
 let mk_bin_string_op = (op: TermBase.UExp.op_bin_string): DHDoc.t =>
   Doc.text(TermBase.UExp.string_op_to_string(op));
 
+let mk_bin_prop_op = (op: TermBase.UExp.op_bin_prop): DHDoc.t =>
+  Doc.text(TermBase.UExp.prop_op_to_string(op));
+
 let mk =
     (
       ~settings: CoreSettings.Evaluation.t,
@@ -151,6 +162,7 @@ let mk =
         | (BinIntOp(_), _)
         | (BinFloatOp(_), _)
         | (BinStringOp(_), _)
+        | (BinPropOp(_), _)
         | (Projection, _)
         | (ListCons, _)
         | (ListConcat, _)
@@ -358,6 +370,7 @@ let mk =
       | FloatLit(f) => DHDoc_common.mk_FloatLit(f)
       | StringLit(s) => DHDoc_common.mk_StringLit(s)
       | PropLit(p) => DHDoc_common.mk_PropLit(p)
+      | JudgementLit(j) => DHDoc_common.mk_JudgementLit(j)
       | Test(_, d) => DHDoc_common.mk_Test(go'(d, Test))
       | Sequence(d1, d2) =>
         let (doc1, doc2) = (go'(d1, Sequence1), go'(d2, Sequence2));
@@ -405,6 +418,14 @@ let mk =
             (d2, BinStringOp2),
           );
         hseps([doc1, mk_bin_string_op(op), doc2]);
+      | BinPropOp(op, d1, d2) =>
+        let (doc1, doc2) =
+          mk_left_associative_operands(
+            DHDoc_common.precedence_Equals,
+            (d1, BinPropOp1),
+            (d2, BinPropOp2),
+          );
+        hseps([doc1, mk_bin_prop_op(op), doc2]);
       | Cons(d1, d2) =>
         let (doc1, doc2) =
           mk_right_associative_operands(
diff --git a/src/haz3lweb/view/dhcode/layout/DHDoc_common.re b/src/haz3lweb/view/dhcode/layout/DHDoc_common.re
index b6e35f8f5c..06c0364605 100644
--- a/src/haz3lweb/view/dhcode/layout/DHDoc_common.re
+++ b/src/haz3lweb/view/dhcode/layout/DHDoc_common.re
@@ -21,6 +21,9 @@ let precedence_And = P.and_;
 let precedence_Or = P.or_;
 let precedence_Comma = P.prod;
 let precedence_max = P.min;
+let precedence_PropAnd = P.prop_and;
+let precedence_PropOr = P.prop_or;
+let precedence_PropImplies = P.prop_implies;
 
 let pad_child =
     (
@@ -106,6 +109,8 @@ let mk_StringLit = s => Doc.text(Form.string_quote(s));
 
 let mk_PropLit = p => Doc.text(Derivation.Prop.repr(p));
 
+let mk_JudgementLit = j => Doc.text(Derivation.Judgement.repr(j));
+
 let mk_Test = t => Doc.(hcats([text("Test"), t, text("End")]));
 
 let mk_FloatLit = (f: float) =>
diff --git a/src/haz3lweb/view/dhcode/layout/DHDoc_common.rei b/src/haz3lweb/view/dhcode/layout/DHDoc_common.rei
index b87344c987..eb21032c68 100644
--- a/src/haz3lweb/view/dhcode/layout/DHDoc_common.rei
+++ b/src/haz3lweb/view/dhcode/layout/DHDoc_common.rei
@@ -17,6 +17,9 @@ let precedence_And: int;
 let precedence_Or: int;
 let precedence_Comma: int;
 let precedence_max: int;
+let precedence_PropAnd: int;
+let precedence_PropOr: int;
+let precedence_PropImplies: int;
 
 let pad_child:
   (
@@ -85,6 +88,8 @@ let mk_StringLit: string => Pretty.Doc.t('a);
 
 let mk_PropLit: Derivation.Prop.t => Pretty.Doc.t('a);
 
+let mk_JudgementLit: Derivation.Judgement.t => Pretty.Doc.t('a);
+
 let mk_Cons: (Pretty.Doc.t('a), Pretty.Doc.t('a)) => Pretty.Doc.t('a);
 
 let mk_ListConcat: (Pretty.Doc.t('a), Pretty.Doc.t('a)) => Pretty.Doc.t('a);
diff --git a/src/haz3lweb/view/dhcode/layout/HTypDoc.re b/src/haz3lweb/view/dhcode/layout/HTypDoc.re
index 90360015db..fd26b405ae 100644
--- a/src/haz3lweb/view/dhcode/layout/HTypDoc.re
+++ b/src/haz3lweb/view/dhcode/layout/HTypDoc.re
@@ -51,6 +51,7 @@ let rec mk = (~parenthesize=false, ~enforce_inline: bool, ty: Typ.t): t => {
     | Bool => (text("Bool"), parenthesize)
     | String => (text("String"), parenthesize)
     | Prop => (text("Prop"), parenthesize)
+    | Judgement => (text("Judgement"), parenthesize)
     | Var(name) => (text(name), parenthesize)
     | List(ty) => (
         hcats([