diff --git a/src/CLI/Print.re b/src/CLI/Print.re
index 8802b66f76..f9fc981678 100644
--- a/src/CLI/Print.re
+++ b/src/CLI/Print.re
@@ -8,6 +8,7 @@ let exp_to_segment_settings: ExpToSegment.Settings.t = {
   fold_case_clauses: false,
   fold_fn_bodies: `NoFold,
   hide_fixpoints: false,
+  show_ascriptions: true,
   show_filters: true,
   show_unknown_as_hole: true,
 };
diff --git a/src/haz3lcore/pretty/ExpToSegment.re b/src/haz3lcore/pretty/ExpToSegment.re
index d28d36e017..6ecd905a8d 100644
--- a/src/haz3lcore/pretty/ExpToSegment.re
+++ b/src/haz3lcore/pretty/ExpToSegment.re
@@ -42,6 +42,7 @@ module Settings = {
     ],
     hide_fixpoints: bool,
     show_filters: bool,
+    show_ascriptions: bool,
     show_unknown_as_hole: bool,
   };
 
@@ -50,6 +51,7 @@ module Settings = {
     parenthesization: Defensive,
     label_format: QuoteWhenNecessary,
     inline,
+    show_ascriptions: settings.evaluation.show_ascriptions,
     fold_case_clauses: !settings.evaluation.show_case_clauses,
     fold_fn_bodies:
       fold_fn_bodies
@@ -69,6 +71,7 @@ module Settings = {
       inline,
       fold_case_clauses: false,
       fold_fn_bodies: `NoFold,
+      show_ascriptions: true,
       hide_fixpoints: false,
       show_filters: true,
       show_unknown_as_hole: true,
@@ -311,13 +314,17 @@ let rec parenthesize =
         (
           ~parenthesization: Settings.parenthesization,
           ~show_filters: bool,
+          ~show_ascriptions: bool,
           ~already_paren=false,
           exp: Exp.t,
         )
         : Exp.t => {
-  let parenthesize = parenthesize(~parenthesization, ~show_filters);
-  let parenthesize_pat = parenthesize_pat(~parenthesization, ~show_filters);
-  let parenthesize_typ = parenthesize_typ(~parenthesization, ~show_filters);
+  let parenthesize =
+    parenthesize(~parenthesization, ~show_filters, ~show_ascriptions);
+  let parenthesize_pat =
+    parenthesize_pat(~parenthesization, ~show_filters, ~show_ascriptions);
+  let parenthesize_typ =
+    parenthesize_typ(~parenthesization, ~show_filters, ~show_ascriptions);
   let paren_at = paren_at(~parenthesization);
   let paren_assoc_at = paren_assoc_at(~parenthesization);
   let paren_pat_at = paren_pat_at(~parenthesization);
@@ -499,12 +506,13 @@ let rec parenthesize =
       parenthesize(e2) |> paren_assoc_at(Precedence.semi),
     )
     |> rewrap
-  | Asc(e, t) =>
+  | Asc(e, t) when show_ascriptions =>
     Asc(
       parenthesize(e) |> paren_assoc_at(Precedence.asc),
       parenthesize_typ(t) |> paren_typ_at(Precedence.asc),
     )
     |> rewrap
+  | Asc(e, _) => parenthesize(e) // skip ascription if not showing
   | Test(e) => Test(parenthesize(e) |> paren_at(Precedence.min)) |> rewrap
   | HintedTest(e, hint) =>
     HintedTest(parenthesize(e) |> paren_at(Precedence.min), hint) |> rewrap
@@ -565,7 +573,10 @@ let rec parenthesize =
     |> rewrap
   | MultiHole(xs) =>
     MultiHole(
-      List.map(parenthesize_any(~parenthesization, ~show_filters), xs),
+      List.map(
+        parenthesize_any(~parenthesization, ~show_ascriptions, ~show_filters),
+        xs,
+      ),
     )
     |> rewrap
   };
@@ -574,12 +585,15 @@ and parenthesize_pat =
     (
       ~parenthesization: Settings.parenthesization,
       ~show_filters: bool,
+      ~show_ascriptions: bool,
       ~already_paren=false,
       pat: Pat.t,
     )
     : Pat.t => {
-  let parenthesize_pat = parenthesize_pat(~parenthesization, ~show_filters);
-  let parenthesize_typ = parenthesize_typ(~parenthesization, ~show_filters);
+  let parenthesize_pat =
+    parenthesize_pat(~parenthesization, ~show_filters, ~show_ascriptions);
+  let parenthesize_typ =
+    parenthesize_typ(~parenthesization, ~show_filters, ~show_ascriptions);
   let paren_pat_at = paren_pat_at(~parenthesization);
   let paren_pat_assoc_at = paren_pat_assoc_at(~parenthesization);
   let paren_typ_at = paren_typ_at(~parenthesization);
@@ -641,15 +655,19 @@ and parenthesize_pat =
     |> rewrap
   | MultiHole(xs) =>
     MultiHole(
-      List.map(parenthesize_any(~parenthesization, ~show_filters), xs),
+      List.map(
+        parenthesize_any(~parenthesization, ~show_ascriptions, ~show_filters),
+        xs,
+      ),
     )
     |> rewrap
-  | Asc(p, t) =>
+  | Asc(p, t) when show_ascriptions =>
     Asc(
       parenthesize_pat(p) |> paren_pat_assoc_at(Precedence.asc),
       parenthesize_typ(t) |> paren_typ_at(Precedence.max) // Hack[Matt]: always add parens to get the arrows right
     )
     |> rewrap
+  | Asc(p, _) => parenthesize_pat(p) // skip ascription if not showing
   };
 }
 
@@ -657,11 +675,13 @@ and parenthesize_typ =
     (
       ~parenthesization: Settings.parenthesization,
       ~show_filters: bool,
+      ~show_ascriptions: bool,
       ~already_paren=false,
       typ: Typ.t,
     )
     : Typ.t => {
-  let parenthesize_typ = parenthesize_typ(~parenthesization, ~show_filters);
+  let parenthesize_typ =
+    parenthesize_typ(~parenthesization, ~show_filters, ~show_ascriptions);
   let paren_typ_at = paren_typ_at(~parenthesization);
   let paren_typ_assoc_at = paren_typ_assoc_at(~parenthesization);
   let paren_at = paren_at(~parenthesization);
@@ -749,7 +769,7 @@ and parenthesize_typ =
     |> rewrap
   | ProofOf(e) =>
     ProofOf(
-      parenthesize(~parenthesization, ~show_filters, e)
+      parenthesize(~parenthesization, ~show_ascriptions, ~show_filters, e)
       |> paren_at(Precedence.min),
     )
     |> rewrap
@@ -774,7 +794,14 @@ and parenthesize_typ =
     Unknown(
       Hole(
         MultiHole(
-          List.map(parenthesize_any(~parenthesization, ~show_filters), xs),
+          List.map(
+            parenthesize_any(
+              ~parenthesization,
+              ~show_ascriptions,
+              ~show_filters,
+            ),
+            xs,
+          ),
         ),
       ),
     )
@@ -786,6 +813,7 @@ and parenthesize_tpat =
     (
       ~parenthesization: Settings.parenthesization,
       ~show_filters: bool,
+      ~show_ascriptions: bool,
       tpat: TPat.t,
     )
     : TPat.t => {
@@ -799,7 +827,10 @@ and parenthesize_tpat =
   // Other forms
   | MultiHole(xs) =>
     MultiHole(
-      List.map(parenthesize_any(~parenthesization, ~show_filters), xs),
+      List.map(
+        parenthesize_any(~parenthesization, ~show_ascriptions, ~show_filters),
+        xs,
+      ),
     )
     |> rewrap
   };
@@ -808,6 +839,7 @@ and parenthesize_tpat =
 and parenthesize_rul =
     (
       ~parenthesization: Settings.parenthesization,
+      ~show_ascriptions: bool,
       ~show_filters: bool,
       rul: Rul.t,
     )
@@ -820,12 +852,22 @@ and parenthesize_rul =
   // Other forms
   | Rules(e, ps) =>
     Rules(
-      parenthesize(~parenthesization, ~show_filters, e),
+      parenthesize(~parenthesization, ~show_ascriptions, ~show_filters, e),
       List.map(
         ((p, e)) =>
           (
-            parenthesize_pat(~parenthesization, ~show_filters, p),
-            parenthesize(~parenthesization, ~show_filters, e),
+            parenthesize_pat(
+              ~parenthesization,
+              ~show_ascriptions,
+              ~show_filters,
+              p,
+            ),
+            parenthesize(
+              ~parenthesization,
+              ~show_ascriptions,
+              ~show_filters,
+              e,
+            ),
           ),
         ps,
       ),
@@ -833,7 +875,10 @@ and parenthesize_rul =
     |> rewrap
   | MultiHole(xs) =>
     MultiHole(
-      List.map(parenthesize_any(~parenthesization, ~show_filters), xs),
+      List.map(
+        parenthesize_any(~parenthesization, ~show_ascriptions, ~show_filters),
+        xs,
+      ),
     )
     |> rewrap
   };
@@ -844,22 +889,59 @@ and parenthesize_any =
       ~parenthesization: Settings.parenthesization,
       ~already_paren=false,
       ~show_filters: bool,
+      ~show_ascriptions: bool,
       any: Any.t,
     )
     : Any.t =>
   switch (any) {
   | Exp(e) =>
-    Exp(parenthesize(~parenthesization, ~already_paren, ~show_filters, e))
+    Exp(
+      parenthesize(
+        ~parenthesization,
+        ~already_paren,
+        ~show_ascriptions,
+        ~show_filters,
+        e,
+      ),
+    )
   | Pat(p) =>
     Pat(
-      parenthesize_pat(~parenthesization, ~already_paren, ~show_filters, p),
+      parenthesize_pat(
+        ~parenthesization,
+        ~already_paren,
+        ~show_ascriptions,
+        ~show_filters,
+        p,
+      ),
     )
   | Typ(t) =>
     Typ(
-      parenthesize_typ(~parenthesization, ~already_paren, ~show_filters, t),
+      parenthesize_typ(
+        ~parenthesization,
+        ~already_paren,
+        ~show_ascriptions,
+        ~show_filters,
+        t,
+      ),
+    )
+  | TPat(tp) =>
+    TPat(
+      parenthesize_tpat(
+        ~parenthesization,
+        ~show_ascriptions,
+        ~show_filters,
+        tp,
+      ),
+    )
+  | Rul(r) =>
+    Rul(
+      parenthesize_rul(
+        ~parenthesization,
+        ~show_ascriptions,
+        ~show_filters,
+        r,
+      ),
     )
-  | TPat(tp) => TPat(parenthesize_tpat(~parenthesization, ~show_filters, tp))
-  | Rul(r) => Rul(parenthesize_rul(~parenthesization, ~show_filters, r))
   | Any(_) => any
   };
 
@@ -1258,6 +1340,7 @@ let rec exp_to_pretty = (~settings: Settings.t, exp: Exp.t): pretty => {
         Pat.fresh(Asc(p, t))
         |> parenthesize_pat(
              ~parenthesization=settings.parenthesization,
+             ~show_ascriptions=settings.show_ascriptions,
              ~show_filters=settings.show_filters,
            );
       };
@@ -2114,6 +2197,7 @@ let exp_to_segment =
          ~parenthesization=settings.parenthesization,
          ~already_paren,
          ~show_filters=settings.show_filters,
+         ~show_ascriptions=settings.show_ascriptions,
        );
   let p = exp_to_pretty(~settings, exp);
   p |> PrettySegment.select;
@@ -2125,6 +2209,7 @@ let typ_to_segment = (~settings: Settings.t, typ: Typ.t): Segment.t => {
     |> parenthesize_typ(
          ~parenthesization=settings.parenthesization,
          ~show_filters=settings.show_filters,
+         ~show_ascriptions=settings.show_ascriptions,
        );
   let p = typ_to_pretty(~settings, typ);
   p |> PrettySegment.select;
@@ -2138,6 +2223,7 @@ let any_to_segment =
          ~parenthesization=settings.parenthesization,
          ~already_paren,
          ~show_filters=settings.show_filters,
+         ~show_ascriptions=settings.show_ascriptions,
        );
   let p = any_to_pretty(~settings, any);
   p |> PrettySegment.select;
diff --git a/src/haz3lcore/zipper/action/Introduce.re b/src/haz3lcore/zipper/action/Introduce.re
index 4f2a3665cb..87382b3305 100644
--- a/src/haz3lcore/zipper/action/Introduce.re
+++ b/src/haz3lcore/zipper/action/Introduce.re
@@ -245,6 +245,7 @@ module Make =
           label_format: QuoteWhenNecessary,
           inline: true,
           fold_case_clauses: false,
+          show_ascriptions: true,
           fold_fn_bodies: `NoFold,
           hide_fixpoints: false,
           show_filters: true,
diff --git a/src/language/CoreSettings.re b/src/language/CoreSettings.re
index 3449bc3eae..1526fb6d1b 100644
--- a/src/language/CoreSettings.re
+++ b/src/language/CoreSettings.re
@@ -7,6 +7,7 @@ module Evaluation = {
     show_fn_bodies: bool,
     show_fixpoints: bool,
     show_ascription_steps: bool,
+    show_ascriptions: bool,
     show_case_steps: bool,
     show_lookup_steps: bool,
     show_stepper_filters: bool,
@@ -22,6 +23,7 @@ module Evaluation = {
     show_fn_bodies: false,
     show_fixpoints: false,
     show_ascription_steps: false,
+    show_ascriptions: false,
     show_case_steps: false,
     show_lookup_steps: false,
     show_stepper_filters: false,
diff --git a/src/web/Settings.re b/src/web/Settings.re
index 8903390d81..ece884c8b0 100644
--- a/src/web/Settings.re
+++ b/src/web/Settings.re
@@ -31,6 +31,7 @@ module Model = {
         show_fn_bodies: false,
         show_fixpoints: false,
         show_ascription_steps: false,
+        show_ascriptions: false,
         show_case_steps: false,
         show_lookup_steps: false,
         show_stepper_filters: false,
@@ -96,6 +97,7 @@ module Update = {
     | ShowCaseClauses
     | ShowFnBodies
     | ShowAscriptionSteps
+    | ShowAscriptions
     | ShowCaseSteps
     | ShowFixpoints
     | ShowLookups
@@ -210,6 +212,10 @@ module Update = {
               ...evaluation,
               show_ascription_steps: !evaluation.show_ascription_steps,
             }
+          | ShowAscriptions => {
+              ...evaluation,
+              show_ascriptions: !evaluation.show_ascriptions,
+            }
           | ShowCaseSteps => {
               ...evaluation,
               show_case_steps: !evaluation.show_case_steps,
diff --git a/src/web/app/editors/SettingsModal.re b/src/web/app/editors/SettingsModal.re
index 6da16ff79d..7de7965980 100644
--- a/src/web/app/editors/SettingsModal.re
+++ b/src/web/app/editors/SettingsModal.re
@@ -41,6 +41,12 @@ let view =
         settings.show_case_clauses,
         Evaluation(ShowCaseClauses),
       ),
+      setting(
+        "⇨",
+        "show case steps",
+        settings.show_case_steps,
+        Evaluation(ShowCaseSteps),
+      ),
       setting(
         "λ",
         "show function bodies",
@@ -53,6 +59,12 @@ let view =
         settings.show_fixpoints,
         Evaluation(ShowFixpoints),
       ),
+      setting(
+        ":",
+        "show ascriptions",
+        settings.show_ascriptions,
+        Evaluation(ShowAscriptions),
+      ),
       setting(
         "⇨",
         "show ascription steps",
diff --git a/src/web/app/inspector/CursorInspector.re b/src/web/app/inspector/CursorInspector.re
index 08c9135b1c..da4dfdbecc 100644
--- a/src/web/app/inspector/CursorInspector.re
+++ b/src/web/app/inspector/CursorInspector.re
@@ -83,6 +83,7 @@ let code_view_settings: Haz3lcore.ExpToSegment.Settings.t = {
   fold_case_clauses: false,
   fold_fn_bodies: `NoFold,
   hide_fixpoints: false,
+  show_ascriptions: true,
   show_filters: false,
   show_unknown_as_hole: true,
 };
diff --git a/src/web/view/ContextInspector.re b/src/web/view/ContextInspector.re
index 179b72cd68..94e1ae7459 100644
--- a/src/web/view/ContextInspector.re
+++ b/src/web/view/ContextInspector.re
@@ -19,6 +19,7 @@ let context_entry_view = (~globals, entry: Language.Ctx.entry): Node.t => {
         fold_case_clauses: false,
         fold_fn_bodies: `NoFold,
         hide_fixpoints: false,
+        show_ascriptions: true,
         show_filters: false,
         show_unknown_as_hole: true,
       },
diff --git a/src/web/view/Kind.re b/src/web/view/Kind.re
index 6ad892b5d3..7c77fca131 100644
--- a/src/web/view/Kind.re
+++ b/src/web/view/Kind.re
@@ -18,6 +18,7 @@ let view = (~globals, kind: Language.Ctx.kind): Node.t =>
             fold_case_clauses: false,
             fold_fn_bodies: `NoFold,
             hide_fixpoints: false,
+            show_ascriptions: true,
             show_filters: false,
             show_unknown_as_hole: true,
           },
diff --git a/src/web/view/NutMenu.re b/src/web/view/NutMenu.re
index c193c5411e..5777fbb6ea 100644
--- a/src/web/view/NutMenu.re
+++ b/src/web/view/NutMenu.re
@@ -66,6 +66,7 @@ let values_group = (~globals: Globals.t) => {
       ("λ", "Functions", s.show_fn_bodies, Evaluation(ShowFnBodies)),
       ("|", "Cases", s.show_case_clauses, Evaluation(ShowCaseClauses)),
       ("f", "Fixpoints", s.show_fixpoints, Evaluation(ShowFixpoints)),
+      (":", "Ascriptions", s.show_ascriptions, Evaluation(ShowAscriptions)),
     ],
   );
 };
diff --git a/test/Test_ExpToSegment.re b/test/Test_ExpToSegment.re
index b9cd5d3bc2..5348339ad6 100644
--- a/test/Test_ExpToSegment.re
+++ b/test/Test_ExpToSegment.re
@@ -12,6 +12,7 @@ let exp_to_segment_settings: ExpToSegment.Settings.t = {
   fold_case_clauses: false,
   fold_fn_bodies: `NoFold,
   hide_fixpoints: false,
+  show_ascriptions: true,
   show_filters: true,
   show_unknown_as_hole: true,
 };
@@ -438,6 +439,7 @@ let exp_to_segment_roundtrip_settings: ExpToSegment.Settings.t = {
   fold_case_clauses: false,
   fold_fn_bodies: `NoFold,
   hide_fixpoints: false,
+  show_ascriptions: true,
   show_filters: true,
   show_unknown_as_hole: true,
 };
@@ -1016,6 +1018,7 @@ let grout_structural_settings: ExpToSegment.Settings.t = {
   fold_case_clauses: false,
   fold_fn_bodies: `NoFold,
   hide_fixpoints: false,
+  show_ascriptions: true,
   show_filters: true,
   show_unknown_as_hole: true,
 };
diff --git a/test/Test_Menhir.re b/test/Test_Menhir.re
index 53ccbbb96b..e060eaa488 100644
--- a/test/Test_Menhir.re
+++ b/test/Test_Menhir.re
@@ -168,6 +168,7 @@ let qcheck_menhir_serialized_equivalent_test =
             inline: true,
             fold_case_clauses: false,
             fold_fn_bodies: `NoFold,
+            show_ascriptions: true,
             hide_fixpoints: false,
             show_filters: true,
             show_unknown_as_hole: true,