diff --git a/src/haz3lcore/pretty/ExpToSegment.re b/src/haz3lcore/pretty/ExpToSegment.re
index 1a048d12a6..9aa603229d 100644
--- a/src/haz3lcore/pretty/ExpToSegment.re
+++ b/src/haz3lcore/pretty/ExpToSegment.re
@@ -33,6 +33,11 @@ let should_add_space = (s1, s2) =>
   | _ when String.starts_with(s2, ~prefix=" ") => false
   | _ when String.ends_with(s1, ~suffix="\n") => false
   | _ when String.starts_with(s2, ~prefix="\n") => false
+  | _
+      when
+        String.ends_with(s1, ~suffix="PROJECTOR")
+        && String.starts_with(s2, ~prefix="(") =>
+    false
   | _
       when
         String.ends_with(s1, ~suffix=")")
@@ -214,7 +219,22 @@ let rec exp_to_pretty = (~settings: Settings.t, exp: Exp.t): pretty => {
     let id = exp |> Exp.rep_id;
     let+ es = es |> List.map(any_to_pretty(~settings)) |> all;
     ListUtil.flat_intersperse(Grout({id, shape: Concave}), es);
-  | Parens({term: Fun(p, e, _, _), _})
+  | Parens({term: Fun(p, e, _, _), _} as inner_exp) =>
+    // TODO: Add optional newlines
+    let id = inner_exp |> Exp.rep_id;
+    let+ p = pat_to_pretty(~settings: Settings.t, p)
+    and+ e = go(e);
+    let name = Exp.get_fn_name(exp) |> Option.value(~default="anon fun");
+    let name =
+      if (settings.hide_fixpoints && String.ends_with(~suffix="+", name)) {
+        String.sub(name, 0, String.length(name) - 1);
+      } else {
+        name;
+      };
+    let name = "<" ++ name ++ ">";
+    let fun_form = [mk_form("fun_", id, [p])] @ e;
+    [mk_form("parens_exp", exp |> Exp.rep_id, [fun_form])]
+    |> fold_fun_if(settings.fold_fn_bodies, name);
   | Fun(p, e, _, _) =>
     // TODO: Add optional newlines
     let id = exp |> Exp.rep_id;
diff --git a/src/haz3lweb/app/editors/result/EvalResult.re b/src/haz3lweb/app/editors/result/EvalResult.re
index 7271553c54..761ac0ad46 100644
--- a/src/haz3lweb/app/editors/result/EvalResult.re
+++ b/src/haz3lweb/app/editors/result/EvalResult.re
@@ -288,7 +288,6 @@ module Selection = {
   type t =
     | Evaluation(CodeSelectable.Selection.t)
     | Stepper(Stepper.Selection.t);
-  // TODO: Selection in stepper
 
   let get_cursor_info = (~selection: t, mr: Model.t): cursor(Update.t) =>
     switch (selection, mr.result) {
diff --git a/src/haz3lweb/app/editors/result/Stepper.re b/src/haz3lweb/app/editors/result/Stepper.re
index f289ae8971..a25ff89b0e 100644
--- a/src/haz3lweb/app/editors/result/Stepper.re
+++ b/src/haz3lweb/app/editors/result/Stepper.re
@@ -175,7 +175,7 @@ module Update = {
     // Only perform below if either previous a or settings have changed
     |> {
       let.calc {expr: _, state, previous_substitutions, next_steps, _} = prev_a
-      and.calc settings = settings;
+      and.calc settings: Calc.t(CoreSettings.t) = settings;
 
       // Check b is valid
       let* b =
@@ -206,7 +206,11 @@ module Update = {
              )
         );
       let next_expr =
-        EvalCtx.compose(b.step.ctx, next_expr) |> Typ.replace_temp_exp;
+        EvalCtx.compose(b.step.ctx, next_expr)
+        |> (
+          settings.evaluation.show_casts ? x => x : Haz3lcore.DHExp.strip_casts
+        )
+        |> Typ.replace_temp_exp;
       let editor = CodeWithStatics.Model.mk_from_exp(~settings, next_expr);
       let next_steps = calc_next_steps(settings, next_expr, next_state);
       (
@@ -293,7 +297,13 @@ module Update = {
             |> {
               let.calc elab = elab
               and.calc settings = settings;
-              let elab = elab |> Typ.replace_temp_exp;
+              let elab =
+                elab
+                |> (
+                  settings.evaluation.show_casts
+                    ? x => x : Haz3lcore.DHExp.strip_casts
+                )
+                |> Typ.replace_temp_exp;
               let editor = CodeWithStatics.Model.mk_from_exp(~settings, elab);
               let next_steps =
                 calc_next_steps(settings, elab, EvaluatorState.init);