From 63ec7cd6cf7ca7b7fdd83d5cf0be25afb81fd3fd Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 16 Dec 2016 19:14:05 -0800
Subject: [PATCH] =?UTF-8?q?chore(library/tools/super):=20replace=20?=
 =?UTF-8?q?=E2=86=A3=20with=20^.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The plan is to delete the funny arrow ↣ notation and keep only ^.
---
 library/tools/super/cdcl.lean               |   8 +-
 library/tools/super/cdcl_solver.lean        | 144 +++++++-------
 library/tools/super/clause.lean             |  54 +++---
 library/tools/super/clause_ops.lean         |  58 +++---
 library/tools/super/clausifier.lean         |  62 +++---
 library/tools/super/datatypes.lean          |  20 +-
 library/tools/super/defs.lean               |   8 +-
 library/tools/super/equality.lean           |  20 +-
 library/tools/super/factoring.lean          |  22 +--
 library/tools/super/inhabited.lean          |  18 +-
 library/tools/super/misc_preprocessing.lean |   8 +-
 library/tools/super/prover.lean             |  10 +-
 library/tools/super/prover_state.lean       | 198 ++++++++++----------
 library/tools/super/resolution.lean         |  40 ++--
 library/tools/super/selection.lean          |  30 +--
 library/tools/super/simp.lean               |   8 +-
 library/tools/super/splitting.lean          |  56 +++---
 library/tools/super/subsumption.lean        |  32 ++--
 library/tools/super/superposition.lean      |  70 +++----
 library/tools/super/utils.lean              |   4 +-
 20 files changed, 435 insertions(+), 435 deletions(-)

diff --git a/library/tools/super/cdcl.lean b/library/tools/super/cdcl.lean
index af3de0bde6..70b965f278 100644
--- a/library/tools/super/cdcl.lean
+++ b/library/tools/super/cdcl.lean
@@ -8,11 +8,11 @@ open tactic expr monad super
 
 private meta def theory_solver_of_tactic (th_solver : tactic unit) : cdcl.solver (option cdcl.proof_term) :=
 do s ← state_t.read, ♯do
-hyps ← return $ s↣trail↣for (λe, e↣hyp),
-subgoal ← mk_meta_var s↣local_false,
+hyps ← return $ s^.trail^.for (λe, e^.hyp),
+subgoal ← mk_meta_var s^.local_false,
 goals ← get_goals,
 set_goals [subgoal],
-hvs ← for hyps (λhyp, assertv hyp↣local_pp_name hyp↣local_type hyp),
+hvs ← for hyps (λhyp, assertv hyp^.local_pp_name hyp^.local_type hyp),
 solved ← (do th_solver, now, return tt) <|> return ff,
 set_goals goals,
 if solved then do
@@ -30,7 +30,7 @@ res ← cdcl.solve (theory_solver_of_tactic th_solver) local_false clauses,
 match res with
 | (cdcl.result.unsat proof) := exact proof
 | (cdcl.result.sat interp) :=
-  let interp' := do e ← interp↣to_list, [if e↣2 = tt then e↣1 else not_ e↣1] in
+  let interp' := do e ← interp^.to_list, [if e.2 = tt then e.1 else not_ e.1] in
   do pp_interp ← pp interp',
      fail (to_fmt "satisfying assignment: " ++ pp_interp)
 end
diff --git a/library/tools/super/cdcl_solver.lean b/library/tools/super/cdcl_solver.lean
index 1b295890a1..0686513a1e 100644
--- a/library/tools/super/cdcl_solver.lean
+++ b/library/tools/super/cdcl_solver.lean
@@ -101,7 +101,7 @@ meta def initial (local_false : expr) : state := {
 }
 
 meta def watches_for (st : state) (pl : prop_lit) : watch_map :=
-(st↣watches↣find pl)↣get_or_else (rb_map.mk _ _)
+(st^.watches^.find pl)^.get_or_else (rb_map.mk _ _)
 
 end state
 
@@ -113,14 +113,14 @@ meta def fail {A B} [has_to_format B] (b : B) : solver A :=
 ♯ @tactic.fail A B _ b
 
 meta def get_local_false : solver expr :=
-do st ← state_t.read, return st↣local_false
+do st ← state_t.read, return st^.local_false
 
 meta def mk_var_core (v : prop_var) (ph : bool) : solver unit := do
-state_t.modify $ λst, match st↣vars↣find v with
+state_t.modify $ λst, match st^.vars^.find v with
 | (some _) := st
 | none := { st with
-    vars := st↣vars↣insert v ⟨ph, none⟩,
-    unassigned := st↣unassigned↣insert v v
+    vars := st^.vars^.insert v ⟨ph, none⟩,
+    unassigned := st^.unassigned^.insert v v
   }
 end
 
@@ -130,36 +130,36 @@ meta def set_conflict (proof : proof_term) : solver unit :=
 state_t.modify $ λst, { st with conflict := some proof }
 
 meta def has_conflict : solver bool :=
-do st ← state_t.read, return st↣conflict↣is_some
+do st ← state_t.read, return st^.conflict^.is_some
 
 meta def push_trail (elem : trail_elem) : solver unit := do
 st ← state_t.read,
-match st↣vars↣find elem↣var with
-| none := fail $ "unknown variable: " ++ elem↣var↣to_string
-| some ⟨_, some _⟩ := fail $ "adding already assigned variable to trail: " ++ elem↣var↣to_string
+match st^.vars^.find elem^.var with
+| none := fail $ "unknown variable: " ++ elem^.var^.to_string
+| some ⟨_, some _⟩ := fail $ "adding already assigned variable to trail: " ++ elem^.var^.to_string
 | some ⟨_, none⟩ :=
   state_t.write { st with
-    vars := st↣vars↣insert elem↣var ⟨elem↣phase, some elem↣hyp⟩,
-    unassigned := st↣unassigned↣erase elem↣var,
-    trail := elem :: st↣trail,
-    unitp_queue := elem↣var :: st↣unitp_queue
+    vars := st^.vars^.insert elem^.var ⟨elem^.phase, some elem^.hyp⟩,
+    unassigned := st^.unassigned^.erase elem^.var,
+    trail := elem :: st^.trail,
+    unitp_queue := elem^.var :: st^.unitp_queue
   }
 end
 
 meta def pop_trail_core : solver (option trail_elem) := do
 st ← state_t.read,
-match st↣trail with
+match st^.trail with
 | elem :: rest := do
   state_t.write { st with trail := rest,
-    vars := st↣vars↣insert elem↣var ⟨elem↣phase, none⟩,
-    unassigned := st↣unassigned↣insert elem↣var elem↣var,
+    vars := st^.vars^.insert elem^.var ⟨elem^.phase, none⟩,
+    unassigned := st^.unassigned^.insert elem^.var elem^.var,
     unitp_queue := [] },
   return $ some elem
 | [] := return none
 end
 
 meta def is_decision_level_zero : solver bool :=
-do st ← state_t.read, return $ st↣trail↣for_all $ λelem, ¬elem↣is_decision
+do st ← state_t.read, return $ st^.trail^.for_all $ λelem, ¬elem^.is_decision
 
 meta def revert_to_decision_level_zero : unit → solver unit | () := do
 is_dl0 ← is_decision_level_zero,
@@ -170,11 +170,11 @@ meta def formula_of_lit (local_false : expr) (v : prop_var) (ph : bool) :=
 if ph then v else imp v local_false
 
 meta def lookup_var (v : prop_var) : solver (option var_state) :=
-do st ← state_t.read, return $ st↣vars↣find v
+do st ← state_t.read, return $ st^.vars^.find v
 
 meta def add_propagation (v : prop_var) (ph : bool) (just : proof_term) (just_is_dn : bool) : solver unit :=
 do v_st ← lookup_var v, local_false ← get_local_false, match v_st with
-| none := fail $ "propagating unknown variable: " ++ v↣to_string
+| none := fail $ "propagating unknown variable: " ++ v^.to_string
 | some ⟨assg_ph, some proof⟩ :=
     if ph = assg_ph then
       return ()
@@ -198,11 +198,11 @@ hyp ← return $ local_const hyp_name hyp_name binder_info.default (formula_of_l
 push_trail $ trail_elem.dec v ph hyp
 
 meta def lookup_lit (l : clause.literal) : solver (option (bool × proof_hyp)) :=
-do var_st_opt ← lookup_var l↣formula, match var_st_opt with
+do var_st_opt ← lookup_var l^.formula, match var_st_opt with
 | none := return none
 | some ⟨ph, none⟩ := return none
 | some ⟨ph, some proof⟩ :=
-  return $ some (if l↣is_neg then bnot ph else ph, proof)
+  return $ some (if l^.is_neg then bnot ph else ph, proof)
 end
 
 meta def lit_is_false (l : clause.literal) : solver bool :=
@@ -215,57 +215,57 @@ meta def lit_is_not_false (l : clause.literal) : solver bool :=
 do isf ← lit_is_false l, return $ bnot isf
 
 meta def cls_is_false (c : clause) : solver bool :=
-lift list.band $ mapm lit_is_false c↣get_lits
+lift list.band $ mapm lit_is_false c^.get_lits
 
 private meta def unit_propg_cls' : clause → solver (option prop_var) | c :=
-if c↣num_lits = 0 then return (some c↣proof)
-else let hd := c↣get_lit 0 in
+if c^.num_lits = 0 then return (some c^.proof)
+else let hd := c^.get_lit 0 in
 do lit_st ← lookup_lit hd, match lit_st with
-| some (ff, isf_prf) := unit_propg_cls' (c↣inst isf_prf)
+| some (ff, isf_prf) := unit_propg_cls' (c^.inst isf_prf)
 | _                  := return none
 end
 
 meta def unit_propg_cls : clause → solver unit | c :=
 do has_confl ← has_conflict,
 if has_confl then return () else
-if c↣num_lits = 0 then do set_conflict c↣proof
-else let hd := c↣get_lit 0 in
+if c^.num_lits = 0 then do set_conflict c^.proof
+else let hd := c^.get_lit 0 in
 do lit_st ← lookup_lit hd, match lit_st with
-| some (ff, isf_prf) := unit_propg_cls (c↣inst isf_prf)
+| some (ff, isf_prf) := unit_propg_cls (c^.inst isf_prf)
 | some (tt, _) := return ()
 | none :=
-do fls_prf_opt ← unit_propg_cls' (c↣inst (expr.mk_var 0)),
+do fls_prf_opt ← unit_propg_cls' (c^.inst (expr.mk_var 0)),
 match fls_prf_opt with
 | some fls_prf := do
-fls_prf' ← return $ lam `H binder_info.default c↣type↣binding_domain fls_prf,
-if hd↣is_neg then
-  add_propagation hd↣formula ff fls_prf' ff
+fls_prf' ← return $ lam `H binder_info.default c^.type^.binding_domain fls_prf,
+if hd^.is_neg then
+  add_propagation hd^.formula ff fls_prf' ff
 else
-  add_propagation hd↣formula tt fls_prf' tt
+  add_propagation hd^.formula tt fls_prf' tt
 | none := return ()
 end
 end
 
 private meta def modify_watches_for (pl : prop_lit) (f : watch_map → watch_map) : solver unit :=
 state_t.modify $ λst, { st with
-  watches := st↣watches↣insert pl $ f $ st↣watches_for pl
+  watches := st^.watches^.insert pl $ f $ st^.watches_for pl
 }
 
 private meta def add_watch (n : name) (c : clause) (i j : ℕ) : solver unit :=
-let l := c↣get_lit i, pl := prop_lit.of_cls_lit l in
-modify_watches_for pl $ λw, w↣insert n (i,j,c)
+let l := c^.get_lit i, pl := prop_lit.of_cls_lit l in
+modify_watches_for pl $ λw, w^.insert n (i,j,c)
 
 private meta def remove_watch (n : name) (c : clause) (i : ℕ) : solver unit :=
-let l := c↣get_lit i, pl := prop_lit.of_cls_lit l in
-modify_watches_for pl $ λw, w↣erase n
+let l := c^.get_lit i, pl := prop_lit.of_cls_lit l in
+modify_watches_for pl $ λw, w^.erase n
 
 private meta def set_watches (n : name) (c : clause) : solver unit :=
-if c↣num_lits = 0 then
-  set_conflict c↣proof
-else if c↣num_lits = 1 then
+if c^.num_lits = 0 then
+  set_conflict c^.proof
+else if c^.num_lits = 1 then
   unit_propg_cls c
 else do
-  not_false_lits ← filter (λi, lit_is_not_false (c↣get_lit i)) (list.range c↣num_lits),
+  not_false_lits ← filter (λi, lit_is_not_false (c^.get_lit i)) (list.range c^.num_lits),
   match not_false_lits with
   | [] := do
       add_watch n c 0 1,
@@ -287,38 +287,38 @@ remove_watch n c i₂,
 set_watches n c
 
 meta def mk_clause (c : clause) : solver unit := do
-c ← ♯c↣distinct,
-for c↣get_lits (λl, mk_var l↣formula),
+c ← ♯c^.distinct,
+for c^.get_lits (λl, mk_var l^.formula),
 revert_to_decision_level_zero (),
-state_t.modify $ λst, { st with clauses := c :: st↣clauses },
+state_t.modify $ λst, { st with clauses := c :: st^.clauses },
 c_name ← ♯mk_fresh_name,
 set_watches c_name c
 
 meta def unit_propg_var (v : prop_var) : solver unit :=
-do st ← state_t.read, if st↣conflict↣is_some then return () else
-match st↣vars↣find v with
-| some ⟨ph, none⟩ := fail $ "propagating unassigned variable: " ++ v↣to_string
-| none := fail $ "unknown variable: " ++ v↣to_string
+do st ← state_t.read, if st^.conflict^.is_some then return () else
+match st^.vars^.find v with
+| some ⟨ph, none⟩ := fail $ "propagating unassigned variable: " ++ v^.to_string
+| none := fail $ "unknown variable: " ++ v^.to_string
 | some ⟨ph, some _⟩ :=
-  let watches := st↣watches_for $ prop_lit.of_var_and_phase v (bnot ph) in
-  for' watches↣to_list $ λw, update_watches w↣1 w↣2↣2↣2 w↣2↣1 w↣2↣2↣1
+  let watches := st^.watches_for $ prop_lit.of_var_and_phase v (bnot ph) in
+  for' watches^.to_list $ λw, update_watches w.1 w.2.2.2 w.2.1 w.2.2.1
 end
 
 meta def analyze_conflict' (local_false : expr) : proof_term → list trail_elem → clause
 | proof (trail_elem.dec v ph hyp :: es) :=
-  let abs_prf := abstract_local proof hyp↣local_uniq_name in
+  let abs_prf := abstract_local proof hyp^.local_uniq_name in
   if has_var abs_prf then
     clause.close_const (analyze_conflict' proof es) hyp
   else
     analyze_conflict' proof es
 | proof (trail_elem.propg v ph l_prf hyp :: es) :=
-  let abs_prf := abstract_local proof hyp↣local_uniq_name in
+  let abs_prf := abstract_local proof hyp^.local_uniq_name in
   if has_var abs_prf then
-    analyze_conflict' (app (lam hyp↣local_pp_name binder_info.default (formula_of_lit local_false v ph) abs_prf) l_prf) es
+    analyze_conflict' (app (lam hyp^.local_pp_name binder_info.default (formula_of_lit local_false v ph) abs_prf) l_prf) es
   else
     analyze_conflict' proof es
 | proof (trail_elem.dbl_neg_propg v ph l_prf hyp :: es) :=
-  let abs_prf := abstract_local proof hyp↣local_uniq_name in
+  let abs_prf := abstract_local proof hyp^.local_uniq_name in
   if has_var abs_prf then
     analyze_conflict' (app l_prf (lambdas [hyp] proof)) es
   else
@@ -326,12 +326,12 @@ meta def analyze_conflict' (local_false : expr) : proof_term → list trail_elem
 | proof [] := ⟨0, 0, proof, local_false, local_false⟩
 
 meta def analyze_conflict (proof : proof_term) : solver clause :=
-do st ← state_t.read, return $ analyze_conflict' st↣local_false proof st↣trail
+do st ← state_t.read, return $ analyze_conflict' st^.local_false proof st^.trail
 
 meta def add_learned (c : clause) : solver unit := do
 prf_abbrev_name ← ♯mk_fresh_name,
-c' ← return { c with proof := local_const prf_abbrev_name prf_abbrev_name binder_info.default c↣type },
-state_t.modify $ λst, { st with learned := ⟨c', c↣proof⟩ :: st↣learned },
+c' ← return { c with proof := local_const prf_abbrev_name prf_abbrev_name binder_info.default c^.type },
+state_t.modify $ λst, { st with learned := ⟨c', c^.proof⟩ :: st^.learned },
 c_name ← ♯mk_fresh_name,
 set_watches c_name c'
 
@@ -341,7 +341,7 @@ if ¬isf then
   state_t.modify (λst, { st with conflict := none })
 else do
   removed_elem ← pop_trail_core,
-  if removed_elem↣is_some then
+  if removed_elem^.is_some then
     backtrack_with conflict_clause
   else
     return ()
@@ -349,14 +349,14 @@ else do
 meta def replace_learned_clauses' : proof_term → list learned_clause → proof_term
 | proof [] := proof
 | proof (⟨c, actual_proof⟩ :: lcs) :=
-  let abs_prf := abstract_local proof c↣proof↣local_uniq_name in
+  let abs_prf := abstract_local proof c^.proof^.local_uniq_name in
   if has_var abs_prf then
-    replace_learned_clauses' (elet c↣proof↣local_pp_name c↣type actual_proof abs_prf) lcs
+    replace_learned_clauses' (elet c^.proof^.local_pp_name c^.type actual_proof abs_prf) lcs
   else
     replace_learned_clauses' proof lcs
 
 meta def replace_learned_clauses (proof : proof_term) : solver proof_term :=
-do st ← state_t.read, return $ replace_learned_clauses' proof st↣learned
+do st ← state_t.read, return $ replace_learned_clauses' proof st^.learned
 
 meta inductive result
 | unsat : proof_term → result
@@ -366,8 +366,8 @@ variable theory_solver : solver (option proof_term)
 
 meta def unit_propg : unit → solver unit | () := do
 st ← state_t.read,
-if st↣conflict↣is_some then return () else
-match st↣unitp_queue with
+if st^.conflict^.is_some then return () else
+match st^.unitp_queue with
 | [] := return ()
 | (v::vs) := do
   state_t.write { st with unitp_queue := vs },
@@ -378,28 +378,28 @@ end
 private meta def run' : unit → solver result | () := do
 unit_propg (),
 st ← state_t.read,
-match st↣conflict with
+match st^.conflict with
 | some conflict := do
   conflict_clause ← analyze_conflict conflict,
-  if conflict_clause↣num_lits = 0 then do
-    proof ← replace_learned_clauses conflict_clause↣proof,
+  if conflict_clause^.num_lits = 0 then do
+    proof ← replace_learned_clauses conflict_clause^.proof,
     return (result.unsat proof)
   else do
     backtrack_with conflict_clause,
     add_learned conflict_clause,
     run' ()
 | none :=
-  match st↣unassigned↣min with
+  match st^.unassigned^.min with
   | none := do
     theory_conflict ← theory_solver,
     match theory_conflict with
     | some conflict := do set_conflict conflict, run' ()
-    | none := return $ result.sat (st↣vars↣for (λvar_st, var_st↣phase))
+    | none := return $ result.sat (st^.vars^.for (λvar_st, var_st^.phase))
     end
   | some unassigned :=
-    match st↣vars↣find unassigned with
+    match st^.vars^.find unassigned with
     | some ⟨ph, none⟩ := do add_decision unassigned ph, run' ()
-    | _ := fail $ "unassigned variable is assigned: " ++ unassigned↣to_string
+    | _ := fail $ "unassigned variable is assigned: " ++ unassigned^.to_string
     end
   end
 end
@@ -408,6 +408,6 @@ meta def run : solver result := run' theory_solver ()
 
 meta def solve (local_false : expr) (clauses : list clause) : tactic result := do
 res ← (do for clauses mk_clause, run theory_solver) (state.initial local_false),
-return res↣1
+return res.1
 
 end cdcl
diff --git a/library/tools/super/clause.lean b/library/tools/super/clause.lean
index b40683cb13..bb59c37d47 100644
--- a/library/tools/super/clause.lean
+++ b/library/tools/super/clause.lean
@@ -26,7 +26,7 @@ namespace clause
 private meta def tactic_format (c : clause) : tactic format := do
 prf_fmt : format ← pp (proof c),
 type_fmt ← pp (type c),
-loc_fls_fmt ← pp c↣local_false,
+loc_fls_fmt ← pp c^.local_false,
 return $ prf_fmt ++ to_fmt " : " ++ type_fmt ++ to_fmt " (" ++
   to_fmt (num_quants c) ++ to_fmt " quants, "
   ++ to_fmt (num_lits c) ++ to_fmt " lits)"
@@ -39,7 +39,7 @@ meta def inst (c : clause) (e : expr) : clause :=
 (if num_quants c > 0
   then mk (num_quants c - 1) (num_lits c)
   else mk 0 (num_lits c - 1))
-(app (proof c) e) (instantiate_var (binding_body (type c)) e) c↣local_false
+(app (proof c) e) (instantiate_var (binding_body (type c)) e) c^.local_false
 
 meta def instn (c : clause) (es : list expr) : clause :=
 foldr (λe c', inst c' e) c es
@@ -59,11 +59,11 @@ match e with
     let abst_type' := abstract_local (type c) (local_uniq_name e) in
     let type' := pi pp binder_info.default t (abstract_local (type c) uniq) in
     let abs_prf := abstract_local (proof c) uniq in
-    let proof' := lambdas [e] c↣proof in
+    let proof' := lambdas [e] c^.proof in
     if num_quants c > 0 ∨ has_var abst_type' then
-      { c with num_quants := c↣num_quants + 1, proof := proof', type := type' }
+      { c with num_quants := c^.num_quants + 1, proof := proof', type := type' }
     else
-      { c with num_lits := c↣num_lits + 1, proof := proof', type := type' }
+      { c with num_lits := c^.num_lits + 1, proof := proof', type := type' }
 | _ := ⟨0, 0, default expr, default expr, default expr⟩
 end
 
@@ -92,8 +92,8 @@ private meta def parse_clause (local_false : expr) : expr → expr → tactic cl
   lc_n ← mk_fresh_name,
   lc ← return $ local_const lc_n n bi d,
   c ← parse_clause (app proof lc) (instantiate_var b lc),
-  return $ c↣close_const $ local_const lc_n n binder_info.default d
-| proof (app (const ``not []) formula) := parse_clause proof (formula↣imp false_)
+  return $ c^.close_const $ local_const lc_n n binder_info.default d
+| proof (app (const ``not []) formula) := parse_clause proof (formula^.imp false_)
 | proof type :=
 if type = local_false then do
   return { num_quants := 0, num_lits := 0, proof := proof, type := type, local_false := local_false }
@@ -133,7 +133,7 @@ meta def is_neg : literal → bool
 | (left _) := tt
 | (right _) := ff
 
-meta def is_pos (l : literal) : bool := bnot l↣is_neg
+meta def is_pos (l : literal) : bool := bnot l^.is_neg
 
 meta def to_formula (l : literal) : tactic expr :=
 if is_neg l then mk_mapp ``not [some (formula l)]
@@ -145,30 +145,30 @@ meta def type_str : literal → string
 
 meta instance : has_to_tactic_format literal :=
 ⟨λl, do
-pp_f ← pp l↣formula,
-return $ to_fmt l↣type_str ++ " (" ++ pp_f ++ ")"⟩
+pp_f ← pp l^.formula,
+return $ to_fmt l^.type_str ++ " (" ++ pp_f ++ ")"⟩
 
 end literal
 
 private meta def get_binding_body : expr → ℕ → expr
 | e 0 := e
-| e (i+1) := get_binding_body e↣binding_body i
+| e (i+1) := get_binding_body e^.binding_body i
 
 meta def get_binder (e : expr) (i : nat) :=
 binding_domain (get_binding_body e i)
 
 meta def validate (c : clause) : tactic unit := do
-concl ← return $ get_binding_body c↣type c↣num_binders,
-unify concl c↣local_false
-      <|> (do pp_concl ← pp concl, pp_lf ← pp c↣local_false,
+concl ← return $ get_binding_body c^.type c^.num_binders,
+unify concl c^.local_false
+      <|> (do pp_concl ← pp concl, pp_lf ← pp c^.local_false,
               fail $ to_fmt "wrong local false: " ++ pp_concl ++ " =!= " ++ pp_lf),
-type' ← infer_type c↣proof,
-unify c↣type type' <|> (do pp_ty ← pp c↣type, pp_ty' ← pp type',
+type' ← infer_type c^.proof,
+unify c^.type type' <|> (do pp_ty ← pp c^.type, pp_ty' ← pp type',
                            fail (to_fmt "wrong type: " ++ pp_ty ++ " =!= " ++ pp_ty'))
 
 meta def get_lit (c : clause) (i : nat) : literal :=
 let bind := get_binder (type c) (num_quants c + i) in
-match is_local_not c↣local_false bind with
+match is_local_not c^.local_false bind with
 | some formula := literal.right formula
 | none         := literal.left bind
 end
@@ -177,10 +177,10 @@ meta def lits_where (c : clause) (p : literal → bool) : list nat :=
 list.filter (λl, p (get_lit c l)) (range (num_lits c))
 
 meta def get_lits (c : clause) : list literal :=
-list.map (get_lit c) (range c↣num_lits)
+list.map (get_lit c) (range c^.num_lits)
 
 meta def is_maximal (gt : expr → expr → bool) (c : clause) (i : nat) : bool :=
-list.empty (list.filter (λj, gt (get_lit c j)↣formula (get_lit c i)↣formula) (range c↣num_lits))
+list.empty (list.filter (λj, gt (get_lit c j)^.formula (get_lit c i)^.formula) (range c^.num_lits))
 
 meta def normalize (c : clause) : tactic clause := do
 opened  ← open_constn c (num_binders c),
@@ -195,9 +195,9 @@ meta def whnf_head_lit (c : clause) : tactic clause := do
 atom' ← whnf $ literal.formula $ get_lit c 0,
 return $
 if literal.is_neg (get_lit c 0) then
-  { c with type := imp atom' (binding_body c↣type) }
+  { c with type := imp atom' (binding_body c^.type) }
 else
-  { c with type := imp (app (const ``not []) atom') c↣type↣binding_body }
+  { c with type := imp (app (const ``not []) atom') c^.type^.binding_body }
 
 end clause
 
@@ -239,16 +239,16 @@ clause.inst_mvars $ clause.close_constn qf' bs
 private meta def distinct' (local_false : expr) : list expr → expr → clause
 | [] proof := ⟨ 0, 0, proof, local_false, local_false ⟩
 | (h::hs) proof :=
-  let (dups, rest) := partition (λh' : expr, h↣local_type = h'↣local_type) hs,
+  let (dups, rest) := partition (λh' : expr, h^.local_type = h'^.local_type) hs,
       proof_wo_dups := foldl (λproof (h' : expr),
-                              instantiate_var (abstract_local proof h'↣local_uniq_name) h)
+                              instantiate_var (abstract_local proof h'^.local_uniq_name) h)
                          proof dups in
-    (distinct' rest proof_wo_dups)↣close_const h
+    (distinct' rest proof_wo_dups)^.close_const h
 
 meta def distinct (c : clause) : tactic clause := do
-(qf, vs) ← c↣open_constn c↣num_quants,
-(fls, hs) ← qf↣open_constn qf↣num_lits,
-return $ (distinct' c↣local_false hs fls↣proof)↣close_constn vs
+(qf, vs) ← c^.open_constn c^.num_quants,
+(fls, hs) ← qf^.open_constn qf^.num_lits,
+return $ (distinct' c^.local_false hs fls^.proof)^.close_constn vs
 
 end clause
 
diff --git a/library/tools/super/clause_ops.lean b/library/tools/super/clause_ops.lean
index 3f35912445..d4f59722d0 100644
--- a/library/tools/super/clause_ops.lean
+++ b/library/tools/super/clause_ops.lean
@@ -12,61 +12,61 @@ meta def on_left_at {m} [monad m] (c : clause) (i : ℕ)
                     [has_monad_lift_t tactic m]
                     -- f gets a type and returns a list of proofs of that type
                     (f : expr → m (list (list expr × expr))) : m (list clause) := do
-op : clause × list expr ← ♯c↣open_constn (c↣num_quants + i),
-♯ @guard tactic _ (op↣1↣get_lit 0)↣is_neg _,
-new_hyps ← f (op↣1↣get_lit 0)↣formula,
-return $ new_hyps↣for (λnew_hyp,
-  (op↣1↣inst new_hyp↣2)↣close_constn (op↣2 ++ new_hyp↣1))
+op : clause × list expr ← ♯c^.open_constn (c^.num_quants + i),
+♯ @guard tactic _ (op.1^.get_lit 0)^.is_neg _,
+new_hyps ← f (op.1^.get_lit 0)^.formula,
+return $ new_hyps^.for (λnew_hyp,
+  (op.1^.inst new_hyp.2)^.close_constn (op.2 ++ new_hyp.1))
 
 meta def on_left_at_dn {m} [monad m] [alternative m] (c : clause) (i : ℕ)
                     [has_monad_lift_t tactic m]
                     -- f gets a hypothesis of ¬type and returns a list of proofs of false
                     (f : expr → m (list (list expr × expr))) : m (list clause) := do
-qf : clause × list expr ← ♯c↣open_constn c↣num_quants,
-op : clause × list expr ← ♯qf↣1↣open_constn c↣num_lits,
-lci ← (op↣2↣nth i)↣to_monad,
-♯ @guard tactic _ (qf↣1↣get_lit i)↣is_neg _,
-h ← ♯ mk_local_def `h $ imp (qf↣1↣get_lit i)↣formula c↣local_false,
+qf : clause × list expr ← ♯c^.open_constn c^.num_quants,
+op : clause × list expr ← ♯qf.1^.open_constn c^.num_lits,
+lci ← (op.2^.nth i)^.to_monad,
+♯ @guard tactic _ (qf.1^.get_lit i)^.is_neg _,
+h ← ♯ mk_local_def `h $ imp (qf.1^.get_lit i)^.formula c^.local_false,
 new_hyps ← f h,
-return $ new_hyps↣for $ λnew_hyp,
-  (((clause.mk 0 0 new_hyp↣2 c↣local_false c↣local_false)↣close_const h)↣inst
-               (op↣1↣close_const lci)↣proof)↣close_constn
-  (qf↣2 ++ op↣2↣remove_nth i ++ new_hyp↣1)
+return $ new_hyps^.for $ λnew_hyp,
+  (((clause.mk 0 0 new_hyp.2 c^.local_false c^.local_false)^.close_const h)^.inst
+               (op.1^.close_const lci)^.proof)^.close_constn
+  (qf.2 ++ op.2^.remove_nth i ++ new_hyp.1)
 
 meta def on_right_at {m} [monad m] (c : clause) (i : ℕ)
                      [has_monad_lift_t tactic m]
                      -- f gets a hypothesis and returns a list of proofs of false
                      (f : expr → m (list (list expr × expr))) : m (list clause) := do
-op : clause × list expr ← ♯c↣open_constn (c↣num_quants + i),
-♯ @guard tactic _ ((op↣1↣get_lit 0)↣is_pos) _,
-h ← ♯ mk_local_def `h (op↣1↣get_lit 0)↣formula,
+op : clause × list expr ← ♯c^.open_constn (c^.num_quants + i),
+♯ @guard tactic _ ((op.1^.get_lit 0)^.is_pos) _,
+h ← ♯ mk_local_def `h (op.1^.get_lit 0)^.formula,
 new_hyps ← f h,
-return $ new_hyps↣for (λnew_hyp,
-  (op↣1↣inst (lambdas [h] new_hyp↣2))↣close_constn (op↣2 ++ new_hyp↣1))
+return $ new_hyps^.for (λnew_hyp,
+  (op.1^.inst (lambdas [h] new_hyp.2))^.close_constn (op.2 ++ new_hyp.1))
 
 meta def on_right_at' {m} [monad m] (c : clause) (i : ℕ)
                      [has_monad_lift_t tactic m]
                      -- f gets a hypothesis and returns a list of proofs
                      (f : expr → m (list (list expr × expr))) : m (list clause) := do
-op : clause × list expr ← ♯c↣open_constn (c↣num_quants + i),
-♯ @guard tactic _ ((op↣1↣get_lit 0)↣is_pos) _,
-h ← ♯ mk_local_def `h (op↣1↣get_lit 0)↣formula,
+op : clause × list expr ← ♯c^.open_constn (c^.num_quants + i),
+♯ @guard tactic _ ((op.1^.get_lit 0)^.is_pos) _,
+h ← ♯ mk_local_def `h (op.1^.get_lit 0)^.formula,
 new_hyps ← f h,
 for new_hyps (λnew_hyp, do
-  type ← ♯ infer_type new_hyp↣2,
-  nh ← ♯ mk_local_def `nh $ imp type c↣local_false,
-  return $ (op↣1↣inst (lambdas [h] (app nh new_hyp↣2)))↣close_constn (op↣2 ++ new_hyp↣1 ++ [nh]))
+  type ← ♯ infer_type new_hyp.2,
+  nh ← ♯ mk_local_def `nh $ imp type c^.local_false,
+  return $ (op.1^.inst (lambdas [h] (app nh new_hyp.2)))^.close_constn (op.2 ++ new_hyp.1 ++ [nh]))
 
 meta def on_first_right (c : clause) (f : expr → tactic (list (list expr × expr))) : tactic (list clause) :=
-first $ do i ← list.range c↣num_lits, [on_right_at c i f]
+first $ do i ← list.range c^.num_lits, [on_right_at c i f]
 
 meta def on_first_right' (c : clause) (f : expr → tactic (list (list expr × expr))) : tactic (list clause) :=
-first $ do i ← list.range c↣num_lits, [on_right_at' c i f]
+first $ do i ← list.range c^.num_lits, [on_right_at' c i f]
 
 meta def on_first_left (c : clause) (f : expr → tactic (list (list expr × expr))) : tactic (list clause) :=
-first $ do i ← list.range c↣num_lits, [on_left_at c i f]
+first $ do i ← list.range c^.num_lits, [on_left_at c i f]
 
 meta def on_first_left_dn (c : clause) (f : expr → tactic (list (list expr × expr))) : tactic (list clause) :=
-first $ do i ← list.range c↣num_lits, [on_left_at_dn c i f]
+first $ do i ← list.range c^.num_lits, [on_left_at_dn c i f]
 
 end super
diff --git a/library/tools/super/clausifier.lean b/library/tools/super/clausifier.lean
index 6d71594569..6a73883c12 100644
--- a/library/tools/super/clausifier.lean
+++ b/library/tools/super/clausifier.lean
@@ -23,26 +23,26 @@ on_first_left c $ λtype, do
 
 meta def inf_whnf_r (c : clause) : tactic (list clause) :=
 on_first_right c $ λha, do
-  a' ← whnf_core transparency.reducible ha↣local_type,
-  guard $ a' ≠ ha↣local_type,
-  hna ← mk_local_def `hna (imp a' c↣local_false),
+  a' ← whnf_core transparency.reducible ha^.local_type,
+  guard $ a' ≠ ha^.local_type,
+  hna ← mk_local_def `hna (imp a' c^.local_false),
   return [([hna], app hna ha)]
 
 set_option eqn_compiler.max_steps 500
 
 meta def inf_false_l (c : clause) : tactic (list clause) :=
-first $ do i ← list.range c↣num_lits,
-  if c↣get_lit i = clause.literal.left false_
+first $ do i ← list.range c^.num_lits,
+  if c^.get_lit i = clause.literal.left false_
   then [return []]
   else []
 
 meta def inf_false_r (c : clause) : tactic (list clause) :=
 on_first_right c $ λhf,
-  if hf↣local_type = c↣local_false
+  if hf^.local_type = c^.local_false
   then return [([], hf)]
-  else match hf↣local_type with
+  else match hf^.local_type with
   | const ``false [] := do
-    pr ← mk_app ``false.rec [c↣local_false, hf],
+    pr ← mk_app ``false.rec [c^.local_false, hf],
     return [([], pr)]
   | _ := failed
   end
@@ -55,8 +55,8 @@ on_first_left c $ λt,
   end
 
 meta def inf_true_r (c : clause) : tactic (list clause) :=
-first $ do i ← list.range c↣num_lits,
-  if c↣get_lit i = clause.literal.right (const ``true [])
+first $ do i ← list.range c^.num_lits,
+  if c^.get_lit i = clause.literal.right (const ``true [])
   then [return []]
   else []
 
@@ -71,9 +71,9 @@ on_first_left c $ λtype,
 
 meta def inf_not_r (c : clause) : tactic (list clause) :=
 on_first_right c $ λhna,
-  match hna↣local_type with
+  match hna^.local_type with
   | app (const ``not []) a := do
-    hnna ← mk_local_def `h (imp (imp a false_) c↣local_false),
+    hnna ← mk_local_def `h (imp (imp a false_) c^.local_false),
     return [([hnna], app hnna hna)]
   | _ := failed
   end
@@ -97,11 +97,11 @@ on_first_right' c $ λhyp, do
 
 meta def inf_or_r (c : clause) : tactic (list clause) :=
 on_first_right c $ λhab,
-  match hab↣local_type with
+  match hab^.local_type with
   | (app (app (const ``or []) a) b) := do
-    hna ← mk_local_def `l (imp a c↣local_false),
-    hnb ← mk_local_def `r (imp b c↣local_false),
-    proof ← mk_app ``or.elim [a, b, c↣local_false, hab, hna, hnb],
+    hna ← mk_local_def `l (imp a c^.local_false),
+    hnb ← mk_local_def `r (imp b c^.local_false),
+    proof ← mk_app ``or.elim [a, b, c^.local_false, hab, hna, hnb],
     return [([hna, hnb], proof)]
   | _ := failed
   end
@@ -120,7 +120,7 @@ on_first_left c $ λab,
 
 meta def inf_all_r (c : clause) : tactic (list clause) :=
 on_first_right' c $ λhallb,
-  match hallb↣local_type with
+  match hallb^.local_type with
   | (pi n bi a b) := do
     ha ← mk_local_def `x a,
     return [([ha], app hallb ha)]
@@ -144,10 +144,10 @@ lemma imp_l_c {F : Prop} {a b} : ((a → b) → F) → ((a → F) → F) :=
 
 meta def inf_imp_l (c : clause) : tactic (list clause) :=
 on_first_left_dn c $ λhnab,
-  match hnab↣local_type with
+  match hnab^.local_type with
   | (pi _ _ (pi _ _ a b) _) :=
-    if b↣has_var then failed else do
-    hna ← mk_local_def `na (imp a c↣local_false),
+    if b^.has_var then failed else do
+    hna ← mk_local_def `na (imp a c^.local_false),
     pf ← first (do r ← [``super.imp_l, ``super.imp_l', ``super.imp_l_c],
                  [mk_app r [hnab, hna]]),
     hb ← mk_local_def `b b,
@@ -178,26 +178,26 @@ assume hab hnenb,
 
 meta def inf_all_l (c : clause) : tactic (list clause) :=
 on_first_left_dn c $ λhnallb,
-  match hnallb↣local_type with
+  match hnallb^.local_type with
   | pi _ _ (pi n bi a b) _ := do
-    enb ← mk_mapp ``Exists [none, some $ lam n binder_info.default a (imp b c↣local_false)],
-    hnenb ← mk_local_def `h (imp enb c↣local_false),
+    enb ← mk_mapp ``Exists [none, some $ lam n binder_info.default a (imp b c^.local_false)],
+    hnenb ← mk_local_def `h (imp enb c^.local_false),
     pr ← mk_app ``super.demorgan' [hnallb, hnenb],
     return [([hnenb], pr)]
   | _ := failed
   end
 
 meta def inf_ex_r  (c : clause) : tactic (list clause) := do
-(qf, ctx) ← c↣open_constn c↣num_quants,
+(qf, ctx) ← c^.open_constn c^.num_quants,
 skolemized ← on_first_right' qf $ λhexp,
-  match hexp↣local_type with
+  match hexp^.local_type with
   | (app (app (const ``Exists [u]) d) p) := do
     sk_sym_name_pp ← get_unused_name `sk (some 1),
     inh_lc ← mk_local' `w binder_info.implicit d,
     sk_sym ← mk_local_def sk_sym_name_pp (pis (ctx ++ [inh_lc]) d),
     sk_p ← whnf_core transparency.none $ app p (app_of_list sk_sym (ctx ++ [inh_lc])),
     sk_ax ← mk_mapp ``Exists [some (local_type sk_sym),
-      some (lambdas [sk_sym] (pis (ctx ++ [inh_lc]) (imp hexp↣local_type sk_p)))],
+      some (lambdas [sk_sym] (pis (ctx ++ [inh_lc]) (imp hexp^.local_type sk_p)))],
     sk_ax_name ← get_unused_name `sk_axiom (some 1), assert sk_ax_name sk_ax,
     nonempt_of_inh ← mk_mapp ``nonempty.intro [some d, some inh_lc],
     eps ← mk_mapp ``classical.epsilon [some d, some nonempt_of_inh, some p],
@@ -209,7 +209,7 @@ skolemized ← on_first_right' qf $ λhexp,
     return [([inh_lc], app_of_list sk_ax' (ctx ++ [inh_lc, hexp]))]
   | _ := failed
   end,
-return $ skolemized↣for (λs, s↣close_constn ctx)
+return $ skolemized^.for (λs, s^.close_constn ctx)
 
 meta def first_some {a : Type} : list (tactic (option a)) → tactic (option a)
 | [] := return none
@@ -219,7 +219,7 @@ private meta def get_clauses_core' (rules : list (clause → tactic (list clause
      : list clause → tactic (list clause) | cs :=
 lift list.join $ do
 for cs $ λc, do first $
-rules↣for (λr, r c >>= get_clauses_core') ++ [return [c]]
+rules^.for (λr, r c >>= get_clauses_core') ++ [return [c]]
 
 meta def get_clauses_core (rules : list (clause → tactic (list clause))) (initial : list clause)
      : tactic (list clause) := do
@@ -268,10 +268,10 @@ monad.for l (clause.of_proof local_false)
 meta def clausification_inf : inf_decl := inf_decl.mk 0 $
 λgiven, list.foldr orelse (return ()) $
         do r ← clausification_rules_classical,
-           [do cs ← ♯ r given↣c,
+           [do cs ← ♯ r given^.c,
                cs' ← ♯ get_clauses_classical cs,
-               for' cs' (λc, mk_derived c given↣sc↣sched_now >>= add_inferred),
-               remove_redundant given↣id []]
+               for' cs' (λc, mk_derived c given^.sc^.sched_now >>= add_inferred),
+               remove_redundant given^.id []]
 
 
 end super
diff --git a/library/tools/super/datatypes.lean b/library/tools/super/datatypes.lean
index 5fc680eb5e..f475057859 100644
--- a/library/tools/super/datatypes.lean
+++ b/library/tools/super/datatypes.lean
@@ -11,12 +11,12 @@ namespace super
 meta def has_diff_constr_eq_l (c : clause) : tactic bool := do
 env ← get_env,
 return $ list.bor $ do
-  l ← c↣get_lits,
-  guard l↣is_neg,
-  return $ match is_eq l↣formula with
+  l ← c^.get_lits,
+  guard l^.is_neg,
+  return $ match is_eq l^.formula with
   | some (lhs, rhs) :=
-    if env↣is_constructor_app lhs ∧ env↣is_constructor_app rhs ∧
-       lhs↣get_app_fn↣const_name ≠ rhs↣get_app_fn↣const_name then
+    if env^.is_constructor_app lhs ∧ env^.is_constructor_app rhs ∧
+       lhs^.get_app_fn^.const_name ≠ rhs^.get_app_fn^.const_name then
       tt
     else
       ff
@@ -24,16 +24,16 @@ return $ list.bor $ do
   end
 
 meta def diff_constr_eq_l_pre := preprocessing_rule $
-filter (λc, lift bnot $♯ has_diff_constr_eq_l c↣c)
+filter (λc, lift bnot $♯ has_diff_constr_eq_l c^.c)
 
 meta def try_no_confusion_eq_r (c : clause) (i : ℕ) : tactic (list clause) :=
 on_right_at' c i $ λhyp,
-  match is_eq hyp↣local_type with
+  match is_eq hyp^.local_type with
   | some (lhs, rhs) := do
     env ← get_env,
     lhs ← whnf lhs, rhs ← whnf rhs,
-    guard $ env↣is_constructor_app lhs ∧ env↣is_constructor_app rhs,
-    pr ← mk_app (lhs↣get_app_fn↣const_name↣get_prefix <.> "no_confusion") [false_, lhs, rhs, hyp],
+    guard $ env^.is_constructor_app lhs ∧ env^.is_constructor_app rhs,
+    pr ← mk_app (lhs^.get_app_fn^.const_name^.get_prefix <.> "no_confusion") [false_, lhs, rhs, hyp],
     -- FIXME: change to local false ^^
     ty ← infer_type pr, ty ← whnf ty,
     pr ← to_expr `(@eq.mpr _ %%ty rfl %%pr), -- FIXME
@@ -43,6 +43,6 @@ on_right_at' c i $ λhyp,
 
 @[super.inf]
 meta def datatype_infs : inf_decl := inf_decl.mk 10 $ take given, do
-sequence' (do i ← list.range given↣c↣num_lits, [inf_if_successful 0 given $ try_no_confusion_eq_r given↣c i])
+sequence' (do i ← list.range given^.c^.num_lits, [inf_if_successful 0 given $ try_no_confusion_eq_r given^.c i])
 
 end super
diff --git a/library/tools/super/defs.lean b/library/tools/super/defs.lean
index 972bbc3fb0..0ef5caa3ee 100644
--- a/library/tools/super/defs.lean
+++ b/library/tools/super/defs.lean
@@ -21,8 +21,8 @@ on_left_at c i $ λt, do
 
 meta def try_unfold_def_right (c : clause) (i : ℕ) : tactic (list clause) :=
 on_right_at c i $ λh, do
-  t' ← try_unfold_one_def h↣local_type,
-  hnt' ← mk_local_def `h (imp t' c↣local_false),
+  t' ← try_unfold_one_def h^.local_type,
+  hnt' ← mk_local_def `h (imp t' c^.local_false),
   return [([hnt'], app hnt' h)]
 
 @[super.inf]
@@ -30,7 +30,7 @@ meta def unfold_def_inf : inf_decl := inf_decl.mk 40 $ take given, sequence' $ d
 r ← [try_unfold_def_right, try_unfold_def_left],
 -- NOTE: we cannot restrict to selected literals here
 -- as this might prevent factoring, e.g. _n>0_ ∨ is_pos(0)
-i ← list.range given↣c↣num_lits,
-[inf_if_successful 3 given (r given↣c i)]
+i ← list.range given^.c^.num_lits,
+[inf_if_successful 3 given (r given^.c i)]
 
 end super
diff --git a/library/tools/super/equality.lean b/library/tools/super/equality.lean
index 11c1f69a01..554d282b67 100644
--- a/library/tools/super/equality.lean
+++ b/library/tools/super/equality.lean
@@ -10,33 +10,33 @@ namespace super
 
 meta def try_unify_eq_l (c : clause) (i : nat) : tactic clause := do
 guard $ clause.literal.is_neg (clause.get_lit c i),
-qf ← clause.open_metan c c↣num_quants,
-match is_eq (qf↣1↣get_lit i)↣formula with
+qf ← clause.open_metan c c^.num_quants,
+match is_eq (qf.1^.get_lit i)^.formula with
 | none := failed
 | some (lhs, rhs) := do
 unify lhs rhs,
 ty ← infer_type lhs,
 univ ← infer_univ ty,
 refl ← return $ app_of_list (const ``eq.refl [univ]) [ty, lhs],
-opened ← clause.open_constn qf↣1 i,
-clause.meta_closure qf↣2 $ clause.close_constn (opened↣1↣inst refl) opened↣2
+opened ← clause.open_constn qf.1 i,
+clause.meta_closure qf.2 $ clause.close_constn (opened.1^.inst refl) opened.2
 end
 
 @[super.inf]
 meta def unify_eq_inf : inf_decl := inf_decl.mk 40 $ take given, sequence' $ do
-i ← given↣selected,
-[inf_if_successful 0 given (do u ← try_unify_eq_l given↣c i, return [u])]
+i ← given^.selected,
+[inf_if_successful 0 given (do u ← try_unify_eq_l given^.c i, return [u])]
 
 meta def has_refl_r (c : clause) : bool :=
 list.bor $ do
-literal ← c↣get_lits,
-guard literal↣is_pos,
-match is_eq literal↣formula with
+literal ← c^.get_lits,
+guard literal^.is_pos,
+match is_eq literal^.formula with
 | some (lhs, rhs) := [decidable.to_bool (lhs = rhs)]
 | none := []
 end
 
 meta def refl_r_pre : prover unit :=
-preprocessing_rule $ take new, return $ filter (λc, ¬has_refl_r c↣c) new
+preprocessing_rule $ take new, return $ filter (λc, ¬has_refl_r c^.c) new
 
 end super
diff --git a/library/tools/super/factoring.lean b/library/tools/super/factoring.lean
index ee39f101ed..628d97c6be 100644
--- a/library/tools/super/factoring.lean
+++ b/library/tools/super/factoring.lean
@@ -15,37 +15,37 @@ opened ← clause.open_constn c i,
 return $ clause.close_constn (clause.inst opened.1 e) opened.2
 
 private meta def try_factor' (c : clause) (i j : nat) : tactic clause := do
-qf ← clause.open_metan c c↣num_quants,
-unify_lit (qf↣1↣get_lit i) (qf↣1↣get_lit j),
+qf ← clause.open_metan c c^.num_quants,
+unify_lit (qf.1^.get_lit i) (qf.1^.get_lit j),
 qfi ← clause.inst_mvars qf.1,
 guard $ clause.is_maximal gt qfi i,
 at_j ← clause.open_constn qf.1 j,
 hyp_i ← option.to_monad (list.nth at_j.2 i),
-clause.meta_closure qf↣2 $ (at_j↣1↣inst hyp_i)↣close_constn at_j↣2
+clause.meta_closure qf.2 $ (at_j.1^.inst hyp_i)^.close_constn at_j.2
 
 meta def try_factor (c : clause) (i j : nat) : tactic clause :=
 if i > j then try_factor' gt c j i else try_factor' gt c i j
 
 meta def try_infer_factor (c : derived_clause) (i j : nat) : prover unit := do
-f ← ♯ try_factor gt c↣c i j,
-ss ← ♯ does_subsume f c↣c,
+f ← ♯ try_factor gt c^.c i j,
+ss ← ♯ does_subsume f c^.c,
 if ss then do
-  f ← mk_derived f c↣sc↣sched_now,
+  f ← mk_derived f c^.sc^.sched_now,
   add_inferred f,
-  remove_redundant c↣id [f]
+  remove_redundant c^.id [f]
 else do
-  inf_score 1 [c↣sc] >>= mk_derived f >>= add_inferred
+  inf_score 1 [c^.sc] >>= mk_derived f >>= add_inferred
 
 @[super.inf]
 meta def factor_inf : inf_decl := inf_decl.mk 40 $
 take given, do gt ← get_term_order, sequence' $ do
-  i ← given↣selected,
-  j ← list.range given↣c↣num_lits,
+  i ← given^.selected,
+  j ← list.range given^.c^.num_lits,
   return $ try_infer_factor gt given i j <|> return ()
 
 meta def factor_dup_lits_pre := preprocessing_rule $ take new, do
 ♯ for new $ λdc, do
-  dist ← dc↣c↣distinct,
+  dist ← dc^.c^.distinct,
   return { dc with c := dist }
 
 end super
diff --git a/library/tools/super/inhabited.lean b/library/tools/super/inhabited.lean
index 1457175306..d9d45131ce 100644
--- a/library/tools/super/inhabited.lean
+++ b/library/tools/super/inhabited.lean
@@ -10,15 +10,15 @@ namespace super
 
 meta def try_nonempty_lookup_left (c : clause) : tactic (list clause) :=
 on_first_left_dn c $ λhnx,
-  match is_local_not c↣local_false hnx↣local_type with
+  match is_local_not c^.local_false hnx^.local_type with
   | some type := do
     univ ← infer_univ type,
-    lf_univ ← infer_univ c↣local_false,
+    lf_univ ← infer_univ c^.local_false,
     guard $ lf_univ = level.zero,
     inst ← mk_instance (app (const ``nonempty [univ]) type),
     instt ← infer_type inst,
     return [([], app_of_list (const ``nonempty.elim [univ])
-                             [type, c↣local_false, inst, hnx])]
+                             [type, c^.local_false, inst, hnx])]
   | _ := failed
   end
 
@@ -33,13 +33,13 @@ on_first_left c $ λprop,
 
 meta def try_nonempty_right (c : clause) : tactic (list clause) :=
 on_first_right c $ λhnonempty,
-  match hnonempty↣local_type with
+  match hnonempty^.local_type with
   | (app (const ``nonempty [u]) type) := do
-    lf_univ ← infer_univ c↣local_false,
+    lf_univ ← infer_univ c^.local_false,
     guard $ lf_univ = level.zero,
-    hnx ← mk_local_def `nx (imp type c↣local_false),
+    hnx ← mk_local_def `nx (imp type c^.local_false),
     return [([hnx], app_of_list (const ``nonempty.elim [u])
-                                [type, c↣local_false, hnonempty, hnx])]
+                                [type, c^.local_false, hnonempty, hnx])]
   | _ := failed
   end
 
@@ -54,7 +54,7 @@ on_first_left c $ λprop,
 
 meta def try_inhabited_right (c : clause) : tactic (list clause) :=
 on_first_right' c $ λhinh,
-  match hinh↣local_type with
+  match hinh^.local_type with
   | (app (const ``inhabited [u]) type) :=
     return [([], app_of_list (const ``inhabited.default [u]) [type, hinh])]
   | _ := failed
@@ -65,6 +65,6 @@ meta def inhabited_infs : inf_decl := inf_decl.mk 10 $ take given, do
 for' [try_nonempty_lookup_left,
        try_nonempty_left, try_nonempty_right,
        try_inhabited_left, try_inhabited_right] $ λr,
-      simp_if_successful given (r given↣c)
+      simp_if_successful given (r given^.c)
 
 end super
diff --git a/library/tools/super/misc_preprocessing.lean b/library/tools/super/misc_preprocessing.lean
index 7ca2fa649e..6f03f68f8d 100644
--- a/library/tools/super/misc_preprocessing.lean
+++ b/library/tools/super/misc_preprocessing.lean
@@ -9,20 +9,20 @@ open expr list monad
 namespace super
 
 meta def is_taut (c : clause) : tactic bool := do
-qf ← c^.open_constn c↣num_quants,
+qf ← c^.open_constn c^.num_quants,
 return $ list.bor $ do
   l1 ← qf^.1^.get_lits, guard l1^.is_neg,
   l2 ← qf^.1^.get_lits, guard l2^.is_pos,
   [decidable.to_bool $ l1^.formula = l2^.formula]
 
 meta def tautology_removal_pre : prover unit :=
-preprocessing_rule $ λnew, filter (λc, lift bnot $♯ is_taut c↣c) new
+preprocessing_rule $ λnew, filter (λc, lift bnot $♯ is_taut c^.c) new
 
 meta def remove_duplicates : list derived_clause → list derived_clause
 | [] := []
 | (c :: cs) :=
-  let (same_type, other_type) := partition (λc' : derived_clause, c'↣c↣type = c↣c↣type) cs in
-  { c with sc := foldl score.min c↣sc (same_type↣for $ λc, c↣sc) } :: remove_duplicates other_type
+  let (same_type, other_type) := partition (λc' : derived_clause, c'^.c^.type = c^.c^.type) cs in
+  { c with sc := foldl score.min c^.sc (same_type^.for $ λc, c^.sc) } :: remove_duplicates other_type
 
 meta def remove_duplicates_pre : prover unit :=
 preprocessing_rule $ λnew,
diff --git a/library/tools/super/prover.lean b/library/tools/super/prover.lean
index 729486c808..b7694e201f 100644
--- a/library/tools/super/prover.lean
+++ b/library/tools/super/prover.lean
@@ -45,16 +45,16 @@ meta def run_prover_loop
 sequence' preprocessing_rules,
 new ← take_newly_derived, for' new register_as_passive,
 ♯ when (is_trace_enabled_for `super) $ for' new $ λn,
-  tactic.trace { n with c := { (n↣c) with proof := const (mk_simple_name " derived") [] } },
-needs_sat_run ← flip monad.lift state_t.read (λst, st↣needs_sat_run),
+  tactic.trace { n with c := { (n^.c) with proof := const (mk_simple_name " derived") [] } },
+needs_sat_run ← flip monad.lift state_t.read (λst, st^.needs_sat_run),
 if needs_sat_run then do
   res ← do_sat_run,
   match res with
   | some proof := return (some proof)
   | none := do
-    model ← flip monad.lift state_t.read (λst, st↣current_model),
+    model ← flip monad.lift state_t.read (λst, st^.current_model),
     ♯ when (is_trace_enabled_for `super) (do
-      pp_model ← pp (model↣to_list↣for (λlit, if lit↣2 = tt then lit↣1 else not_ lit↣1)),
+      pp_model ← pp (model^.to_list^.for (λlit, if lit.2 = tt then lit.1 else not_ lit.1)),
       trace $ to_fmt "sat model: " ++ pp_model),
     run_prover_loop i
   end
@@ -110,7 +110,7 @@ namespace tactic.interactive
 meta def with_lemmas (ls : types.raw_ident_list) : tactic unit := monad.for' ls $ λl, do
 p ← mk_const l,
 t ← infer_type p,
-n ← get_unused_name p↣get_app_fn↣const_name none,
+n ← get_unused_name p^.get_app_fn^.const_name none,
 tactic.assertv n t p
 
 meta def super (extra_clause_names : types.raw_ident_list)
diff --git a/library/tools/super/prover_state.lean b/library/tools/super/prover_state.lean
index 3277e144ff..29c65eeea1 100644
--- a/library/tools/super/prover_state.lean
+++ b/library/tools/super/prover_state.lean
@@ -22,27 +22,27 @@ def prio.never     : ℕ := 2
 def sched_default (sc : score) : score := { sc with priority := prio.default }
 def sched_now (sc : score) : score := { sc with priority := prio.immediate }
 
-def inc_cost (sc : score) (n : ℕ) : score := { sc with cost := sc↣cost + n }
+def inc_cost (sc : score) (n : ℕ) : score := { sc with cost := sc^.cost + n }
 
 def min (a b : score) : score :=
-{ priority := nat.min a↣priority b↣priority,
-  in_sos := a↣in_sos && b↣in_sos,
-  cost := nat.min a↣cost b↣cost,
-  age := nat.min a↣age b↣age }
+{ priority := nat.min a^.priority b^.priority,
+  in_sos := a^.in_sos && b^.in_sos,
+  cost := nat.min a^.cost b^.cost,
+  age := nat.min a^.age b^.age }
 
 def combine (a b : score) : score :=
-{ priority := nat.max a↣priority b↣priority,
-  in_sos := a↣in_sos && b↣in_sos,
-  cost := a↣cost + b↣cost,
-  age := nat.max a↣age b↣age }
+{ priority := nat.max a^.priority b^.priority,
+  in_sos := a^.in_sos && b^.in_sos,
+  cost := a^.cost + b^.cost,
+  age := nat.max a^.age b^.age }
 end score
 
 namespace score
 meta instance : has_to_string score :=
-⟨λe, "[" ++ to_string e↣priority ++
-     "," ++ to_string e↣cost ++
-     "," ++ to_string e↣age ++
-     ",sos=" ++ to_string e↣in_sos ++ "]"⟩
+⟨λe, "[" ++ to_string e^.priority ++
+     "," ++ to_string e^.cost ++
+     "," ++ to_string e^.age ++
+     ",sos=" ++ to_string e^.in_sos ++ "]"⟩
 end score
 
 def clause_id := ℕ
@@ -63,17 +63,17 @@ namespace derived_clause
 
 meta instance : has_to_tactic_format derived_clause :=
 ⟨λc, do
-c_fmt ← pp c↣c,
-ass_fmt ← pp (c↣assertions↣for (λa, a↣local_type)),
+c_fmt ← pp c^.c,
+ass_fmt ← pp (c^.assertions^.for (λa, a^.local_type)),
 return $
-to_string c↣sc ++ " " ++
+to_string c^.sc ++ " " ++
 c_fmt ++ " <- " ++ ass_fmt ++
-" (selected: " ++ to_fmt c↣selected ++
+" (selected: " ++ to_fmt c^.selected ++
 ")"
 ⟩
 
 meta def clause_with_assertions (ac : derived_clause) : clause :=
-ac↣c↣close_constn ac↣assertions
+ac^.c^.close_constn ac^.assertions
 
 end derived_clause
 
@@ -85,8 +85,8 @@ namespace locked_clause
 
 meta instance : has_to_tactic_format locked_clause :=
 ⟨λc, do
-c_fmt ← pp c↣dc,
-reasons_fmt ← pp (c↣reasons↣for (λr, r↣for (λa, a↣local_type))),
+c_fmt ← pp c^.dc,
+reasons_fmt ← pp (c^.reasons^.for (λr, r^.for (λa, a^.local_type))),
 return $ c_fmt ++ " (locked in case of: " ++ reasons_fmt ++ ")"
 ⟩
 
@@ -111,12 +111,12 @@ private meta def join_with_nl : list format → format :=
 list.foldl (λx y, x ++ format.line ++ y) format.nil
 
 private meta def prover_state_tactic_fmt (s : prover_state) : tactic format := do
-active_fmts ← mapm pp $ rb_map.values s↣active,
-passive_fmts ← mapm pp $ rb_map.values s↣passive,
-new_fmts ← mapm pp s↣newly_derived,
-locked_fmts ← mapm pp s↣locked,
-sat_fmts ← mapm pp s↣sat_solver↣clauses,
-prec_fmts ← mapm pp s↣prec,
+active_fmts ← mapm pp $ rb_map.values s^.active,
+passive_fmts ← mapm pp $ rb_map.values s^.passive,
+new_fmts ← mapm pp s^.newly_derived,
+locked_fmts ← mapm pp s^.locked,
+sat_fmts ← mapm pp s^.sat_solver^.clauses,
+prec_fmts ← mapm pp s^.prec,
 return (join_with_nl
   ([to_fmt "active:"] ++ map (append (to_fmt "  ")) active_fmts ++
   [to_fmt "passive:"] ++ map (append (to_fmt "  ")) passive_fmts ++
@@ -150,21 +150,21 @@ alternative.mk (@monad.map _ _)
 meta def selection_strategy := derived_clause → prover derived_clause
 
 meta def get_active : prover (rb_map clause_id derived_clause) :=
-do state ← state_t.read, return state↣active
+do state ← state_t.read, return state^.active
 
 meta def add_active (a : derived_clause) : prover unit :=
 do state ← state_t.read,
-state_t.write { state with active := state↣active↣insert a↣id a }
+state_t.write { state with active := state^.active^.insert a^.id a }
 
 meta def get_passive : prover (rb_map clause_id derived_clause) :=
 lift passive state_t.read
 
 meta def get_precedence : prover (list expr) :=
-do state ← state_t.read, return state↣prec
+do state ← state_t.read, return state^.prec
 
 meta def get_term_order : prover (expr → expr → bool) := do
 state ← state_t.read,
-return $ lpo (prec_gt_of_name_list (map name_of_funsym state↣prec))
+return $ lpo (prec_gt_of_name_list (map name_of_funsym state^.prec))
 
 private meta def set_precedence (new_prec : list expr) : prover unit :=
 do state ← state_t.read, state_t.write { state with prec := new_prec }
@@ -172,31 +172,31 @@ do state ← state_t.read, state_t.write { state with prec := new_prec }
 meta def register_consts_in_precedence (consts : list expr) := do
 p ← get_precedence,
 p_set ← return (rb_map.set_of_list (map name_of_funsym p)),
-new_syms ← return $ list.filter (λc, ¬p_set↣contains (name_of_funsym c)) consts,
+new_syms ← return $ list.filter (λc, ¬p_set^.contains (name_of_funsym c)) consts,
 set_precedence (new_syms ++ p)
 
 meta def in_sat_solver {A} (cmd : cdcl.solver A) : prover A := do
 state ← state_t.read,
-result ← ♯ cmd state↣sat_solver,
-state_t.write { state with sat_solver := result↣2 },
-return result↣1
+result ← ♯ cmd state^.sat_solver,
+state_t.write { state with sat_solver := result.2 },
+return result.1
 
 meta def collect_ass_hyps (c : clause) : prover (list expr) :=
-let lcs := contained_lconsts c↣proof in
+let lcs := contained_lconsts c^.proof in
 do st ← state_t.read,
 return (do
-  hs ← st↣sat_hyps↣values,
-  h ← [hs↣1, hs↣2],
-  guard $ lcs↣contains h↣local_uniq_name,
+  hs ← st^.sat_hyps^.values,
+  h ← [hs.1, hs.2],
+  guard $ lcs^.contains h^.local_uniq_name,
   [h])
 
 meta def get_clause_count : prover ℕ :=
-do s ← state_t.read, return s↣clause_counter
+do s ← state_t.read, return s^.clause_counter
 
 meta def get_new_cls_id : prover clause_id := do
 state ← state_t.read,
-state_t.write { state with clause_counter := state↣clause_counter + 1 },
-return state↣clause_counter
+state_t.write { state with clause_counter := state^.clause_counter + 1 },
+return state^.clause_counter
 
 meta def mk_derived (c : clause) (sc : score) : prover derived_clause := do
 ass ← collect_ass_hyps c,
@@ -204,31 +204,31 @@ id ← ♯ get_new_cls_id,
 return { id := id, c := c, selected := [], assertions := ass, sc := sc }
 
 meta def add_inferred (c : derived_clause) : prover unit := do
-c' ← ♯c↣c↣normalize, c' ← return { c with c := c' },
-register_consts_in_precedence (contained_funsyms c'↣c↣type)↣values,
+c' ← ♯c^.c^.normalize, c' ← return { c with c := c' },
+register_consts_in_precedence (contained_funsyms c'^.c^.type)^.values,
 state ← state_t.read,
-state_t.write { state with newly_derived := c' :: state↣newly_derived }
+state_t.write { state with newly_derived := c' :: state^.newly_derived }
 
 
 
 -- FIXME: what if we've seen the variable before, but with a weaker score?
 meta def mk_sat_var (v : expr) (suggested_ph : bool) (suggested_ev : score) : prover unit :=
-do st ← state_t.read, if st↣sat_hyps↣contains v then return () else do
+do st ← state_t.read, if st^.sat_hyps^.contains v then return () else do
 hpv ← ♯ mk_local_def `h v,
-hnv ← ♯ mk_local_def `hn $ imp v st↣local_false,
-state_t.modify $ λst, { st with sat_hyps := st↣sat_hyps↣insert v (hpv, hnv) },
+hnv ← ♯ mk_local_def `hn $ imp v st^.local_false,
+state_t.modify $ λst, { st with sat_hyps := st^.sat_hyps^.insert v (hpv, hnv) },
 in_sat_solver $ cdcl.mk_var_core v suggested_ph,
 match v with
 | (pi _ _ _ _) := do
-  c ← ♯ clause.of_proof st↣local_false hpv,
+  c ← ♯ clause.of_proof st^.local_false hpv,
   mk_derived c suggested_ev >>= add_inferred
-| _ := do cp ← ♯ clause.of_proof st↣local_false hpv, mk_derived cp suggested_ev >>= add_inferred,
-          cn ← ♯ clause.of_proof st↣local_false hnv, mk_derived cn suggested_ev >>= add_inferred
+| _ := do cp ← ♯ clause.of_proof st^.local_false hpv, mk_derived cp suggested_ev >>= add_inferred,
+          cn ← ♯ clause.of_proof st^.local_false hnv, mk_derived cn suggested_ev >>= add_inferred
 end
 
 meta def get_sat_hyp_core (v : expr) (ph : bool) : prover (option expr) :=
 flip monad.lift state_t.read $ λst,
-  match st↣sat_hyps↣find v with
+  match st^.sat_hyps^.find v with
   | some (hp, hn) := some $ if ph then hp else hn
   | none := none
   end
@@ -237,30 +237,30 @@ meta def get_sat_hyp (v : expr) (ph : bool) : prover expr :=
 do hyp_opt ← get_sat_hyp_core v ph,
 match hyp_opt with
 | some hyp := return hyp
-| none := prover.fail $ "unknown sat variable: " ++ v↣to_string
+| none := prover.fail $ "unknown sat variable: " ++ v^.to_string
 end
 
 meta def add_sat_clause (c : clause) (suggested_ev : score) : prover unit := do
-c ← ♯ c↣distinct,
+c ← ♯ c^.distinct,
 already_added ← flip monad.lift state_t.read $ λst, decidable.to_bool $
-                     c↣type ∈ st↣sat_solver↣clauses↣for (λd, d↣type),
+                     c^.type ∈ st^.sat_solver^.clauses^.for (λd, d^.type),
 if already_added then return () else do
-for c↣get_lits $ λl, mk_sat_var l↣formula l↣is_neg suggested_ev,
+for c^.get_lits $ λl, mk_sat_var l^.formula l^.is_neg suggested_ev,
 in_sat_solver $ cdcl.mk_clause c,
 state_t.modify $ λst, { st with needs_sat_run := tt }
 
 meta def sat_eval_lit (v : expr) (pol : bool) : prover bool :=
-do v_st ← flip monad.lift state_t.read $ λst, st↣current_model↣find v,
+do v_st ← flip monad.lift state_t.read $ λst, st^.current_model^.find v,
 match v_st with
 | some ph := return $ if pol then ph else bnot ph
 | none := return tt
 end
 
 meta def sat_eval_assertion (assertion : expr) : prover bool :=
-do lf ← flip monad.lift state_t.read $ λst, st↣local_false,
-match is_local_not lf assertion↣local_type with
+do lf ← flip monad.lift state_t.read $ λst, st^.local_false,
+match is_local_not lf assertion^.local_type with
 | some v := sat_eval_lit v ff
-| none := sat_eval_lit assertion↣local_type tt
+| none := sat_eval_lit assertion^.local_type tt
 end
 
 meta def sat_eval_assertions : list expr → prover bool
@@ -272,33 +272,33 @@ return ff
 | [] := return tt
 
 private meta def intern_clause (c : derived_clause) : prover derived_clause := do
-hyp_name ← ♯ get_unused_name (mk_simple_name $ "clause_" ++ to_string c↣id↣to_nat) none,
-c' ← return $ c↣c↣close_constn c↣assertions,
-♯ assertv hyp_name c'↣type c'↣proof,
+hyp_name ← ♯ get_unused_name (mk_simple_name $ "clause_" ++ to_string c^.id^.to_nat) none,
+c' ← return $ c^.c^.close_constn c^.assertions,
+♯ assertv hyp_name c'^.type c'^.proof,
 proof' ← ♯ get_local hyp_name,
 type ← ♯ infer_type proof', -- FIXME: otherwise ""
-return { c with c := { (c↣c : clause) with proof := app_of_list proof' c↣assertions } }
+return { c with c := { (c^.c : clause) with proof := app_of_list proof' c^.assertions } }
 
 meta def register_as_passive (c : derived_clause) : prover unit := do
 c ← intern_clause c,
-ass_v ← sat_eval_assertions c↣assertions,
-if c↣c↣num_quants = 0 ∧ c↣c↣num_lits = 0 then
-  add_sat_clause c↣clause_with_assertions c↣sc
+ass_v ← sat_eval_assertions c^.assertions,
+if c^.c^.num_quants = 0 ∧ c^.c^.num_lits = 0 then
+  add_sat_clause c^.clause_with_assertions c^.sc
 else if ¬ass_v then do
-  state_t.modify $ λst, { st with locked := ⟨c, []⟩ :: st↣locked }
+  state_t.modify $ λst, { st with locked := ⟨c, []⟩ :: st^.locked }
 else do
-  state_t.modify $ λst, { st with passive := st↣passive↣insert c↣id c }
+  state_t.modify $ λst, { st with passive := st^.passive^.insert c^.id c }
 
 meta def remove_passive (id : clause_id) : prover unit :=
-do state ← state_t.read, state_t.write { state with passive := state↣passive↣erase id }
+do state ← state_t.read, state_t.write { state with passive := state^.passive^.erase id }
 
 meta def move_locked_to_passive : prover unit := do
-locked ← flip monad.lift state_t.read (λst, st↣locked),
+locked ← flip monad.lift state_t.read (λst, st^.locked),
 new_locked ← flip filter locked (λlc, do
-  reason_vals ← mapm sat_eval_assertions lc↣reasons,
-  c_val ← sat_eval_assertions lc↣dc↣assertions,
-  if reason_vals↣for_all (λr, r = ff) ∧ c_val then do
-    state_t.modify $ λst, { st with passive := st↣passive↣insert lc↣dc↣id lc↣dc },
+  reason_vals ← mapm sat_eval_assertions lc^.reasons,
+  c_val ← sat_eval_assertions lc^.dc^.assertions,
+  if reason_vals^.for_all (λr, r = ff) ∧ c_val then do
+    state_t.modify $ λst, { st with passive := st^.passive^.insert lc^.dc^.id lc^.dc },
     return ff
   else
     return tt
@@ -306,23 +306,23 @@ new_locked ← flip filter locked (λlc, do
 state_t.modify $ λst, { st with locked := new_locked }
 
 meta def move_active_to_locked : prover unit :=
-do active ← get_active, for' active↣values $ λac, do
-  c_val ← sat_eval_assertions ac↣assertions,
+do active ← get_active, for' active^.values $ λac, do
+  c_val ← sat_eval_assertions ac^.assertions,
   if ¬c_val then do
      state_t.modify $ λst, { st with
-       active := st↣active↣erase ac↣id,
-       locked := ⟨ac, []⟩ :: st↣locked
+       active := st^.active^.erase ac^.id,
+       locked := ⟨ac, []⟩ :: st^.locked
      }
   else
     return ()
 
 meta def move_passive_to_locked : prover unit :=
-do passive ← flip monad.lift state_t.read $ λst, st↣passive, for' passive↣to_list $ λpc, do
-  c_val ← sat_eval_assertions pc↣2↣assertions,
+do passive ← flip monad.lift state_t.read $ λst, st^.passive, for' passive^.to_list $ λpc, do
+  c_val ← sat_eval_assertions pc.2^.assertions,
   if ¬c_val then do
     state_t.modify $ λst, { st with
-      passive := st↣passive↣erase pc↣1,
-      locked := ⟨pc↣2, []⟩ :: st↣locked
+      passive := st^.passive^.erase pc.1,
+      locked := ⟨pc.2, []⟩ :: st^.locked
     }
   else
     return ()
@@ -344,21 +344,21 @@ end
 meta def take_newly_derived : prover (list derived_clause) := do
 state ← state_t.read,
 state_t.write { state with newly_derived := [] },
-return state↣newly_derived
+return state^.newly_derived
 
 meta def remove_redundant (id : clause_id) (parents : list derived_clause) : prover unit := do
-guard $ parents↣for_all $ λp, p↣id ≠ id,
-red ← flip monad.lift state_t.read (λst, st↣active↣find id),
+guard $ parents^.for_all $ λp, p^.id ≠ id,
+red ← flip monad.lift state_t.read (λst, st^.active^.find id),
 match red with
 | none := return ()
 | some red := do
-let reasons := parents↣for (λp, p↣assertions),
-    assertion := red↣assertions in
-if reasons↣for_all $ λr, r↣subset_of assertion then do
-  state_t.modify $ λst, { st with active := st↣active↣erase id }
+let reasons := parents^.for (λp, p^.assertions),
+    assertion := red^.assertions in
+if reasons^.for_all $ λr, r^.subset_of assertion then do
+  state_t.modify $ λst, { st with active := st^.active^.erase id }
 else do
-  state_t.modify $ λst, { st with active := st↣active↣erase id,
-                                 locked := ⟨red, reasons⟩ :: st↣locked }
+  state_t.modify $ λst, { st with active := st^.active^.erase id,
+                                 locked := ⟨red, reasons⟩ :: st^.locked }
 end
 
 meta def inference := derived_clause → prover unit
@@ -372,7 +372,7 @@ meta def seq_inferences : list inference → inference
 | (inf::infs) := λgiven, do
     inf given,
     now_active ← get_active,
-    if rb_map.contains now_active given↣id then
+    if rb_map.contains now_active given^.id then
       seq_inferences infs given
     else
       return ()
@@ -381,15 +381,15 @@ meta def simp_inference (simpl : derived_clause → prover (option clause)) : in
 λgiven, do maybe_simpld ← simpl given,
 match maybe_simpld with
 | some simpld := do
-  derived_simpld ← mk_derived simpld given↣sc↣sched_now,
+  derived_simpld ← mk_derived simpld given^.sc^.sched_now,
   add_inferred derived_simpld,
-  remove_redundant given↣id []
+  remove_redundant given^.id []
 | none := return ()
 end
 
 meta def preprocessing_rule (f : list derived_clause → prover (list derived_clause)) : prover unit := do
 state ← state_t.read,
-newly_derived' ← f state↣newly_derived,
+newly_derived' ← f state^.newly_derived,
 state' ← state_t.read,
 state_t.write { state' with newly_derived := newly_derived' }
 
@@ -406,7 +406,7 @@ meta def empty (local_false : expr) : prover_state :=
 
 meta def initial (local_false : expr) (clauses : list clause) : tactic prover_state := do
 after_setup ← for' clauses (λc,
-  let in_sos := decidable.to_bool ((contained_lconsts c↣proof)↣size = 0) in
+  let in_sos := decidable.to_bool ((contained_lconsts c^.proof)^.size = 0) in
   do mk_derived c { priority := score.prio.immediate, in_sos := in_sos,
                     age := 0, cost := 0 } >>= add_inferred
 ) $ empty local_false,
@@ -425,14 +425,14 @@ return $ list.foldl score.combine { priority := score.prio.default,
 meta def inf_if_successful (add_cost : ℕ) (parent : derived_clause) (tac : tactic (list clause)) : prover unit :=
 (do inferred ← ♯tac,
     for' inferred $ λc,
-      inf_score add_cost [parent↣sc] >>= mk_derived c >>= add_inferred)
+      inf_score add_cost [parent^.sc] >>= mk_derived c >>= add_inferred)
 <|> return ()
 
 meta def simp_if_successful (parent : derived_clause) (tac : tactic (list clause)) : prover unit :=
 (do inferred ← ♯tac,
     for' inferred $ λc,
-      mk_derived c parent↣sc↣sched_now >>= add_inferred,
-    remove_redundant parent↣id [])
+      mk_derived c parent^.sc^.sched_now >>= add_inferred,
+    remove_redundant parent^.id [])
 <|> return ()
 
 end super
diff --git a/library/tools/super/resolution.lean b/library/tools/super/resolution.lean
index 58ebbec274..a12a1dd7e1 100644
--- a/library/tools/super/resolution.lean
+++ b/library/tools/super/resolution.lean
@@ -16,43 +16,43 @@ variables (i1 i2 : nat)
 -- c1 : ... → ¬a → ...
 -- c2 : ... →  a → ...
 meta def try_resolve : tactic clause := do
-qf1 ← c1↣open_metan c1↣num_quants,
-qf2 ← c2↣open_metan c2↣num_quants,
+qf1 ← c1^.open_metan c1^.num_quants,
+qf2 ← c2^.open_metan c2^.num_quants,
 -- FIXME: using default transparency unifies m*n with (x*y*z)*w here ???
-unify_core transparency.reducible (qf1↣1↣get_lit i1)↣formula (qf2↣1↣get_lit i2)↣formula,
-qf1i ← qf1↣1↣inst_mvars,
+unify_core transparency.reducible (qf1.1^.get_lit i1)^.formula (qf2.1^.get_lit i2)^.formula,
+qf1i ← qf1.1^.inst_mvars,
 guard $ clause.is_maximal gt qf1i i1,
-op1 ← qf1↣1↣open_constn i1,
-op2 ← qf2↣1↣open_constn c2↣num_lits,
-a_in_op2 ← (op2↣2↣nth i2)↣to_monad,
+op1 ← qf1.1^.open_constn i1,
+op2 ← qf2.1^.open_constn c2^.num_lits,
+a_in_op2 ← (op2.2^.nth i2)^.to_monad,
 clause.meta_closure (qf1.2 ++ qf2.2) $
-  (op1↣1↣inst (op2↣1↣close_const a_in_op2)↣proof)↣close_constn (op1↣2 ++ op2↣2↣remove_nth i2)
+  (op1.1^.inst (op2.1^.close_const a_in_op2)^.proof)^.close_constn (op1.2 ++ op2.2^.remove_nth i2)
 
 meta def try_add_resolvent : prover unit := do
-c' ← ♯ try_resolve gt ac1↣c ac2↣c i1 i2,
-inf_score 1 [ac1↣sc, ac2↣sc] >>= mk_derived c' >>= add_inferred
+c' ← ♯ try_resolve gt ac1^.c ac2^.c i1 i2,
+inf_score 1 [ac1^.sc, ac2^.sc] >>= mk_derived c' >>= add_inferred
 
 meta def maybe_add_resolvent : prover unit :=
 try_add_resolvent gt ac1 ac2 i1 i2 <|> return ()
 
 meta def resolution_left_inf : inference :=
 take given, do active ← get_active, sequence' $ do
-  given_i ← given↣selected,
-  guard $ clause.literal.is_neg (given↣c↣get_lit given_i),
+  given_i ← given^.selected,
+  guard $ clause.literal.is_neg (given^.c^.get_lit given_i),
   other ← rb_map.values active,
-  guard $ ¬given↣sc↣in_sos ∨ ¬other↣sc↣in_sos,
-  other_i ← other↣selected,
-  guard $ clause.literal.is_pos (other↣c↣get_lit other_i),
+  guard $ ¬given^.sc^.in_sos ∨ ¬other^.sc^.in_sos,
+  other_i ← other^.selected,
+  guard $ clause.literal.is_pos (other^.c^.get_lit other_i),
   [maybe_add_resolvent gt other given other_i given_i]
 
 meta def resolution_right_inf : inference :=
 take given, do active ← get_active, sequence' $ do
-  given_i ← given↣selected,
-  guard $ clause.literal.is_pos (given↣c↣get_lit given_i),
+  given_i ← given^.selected,
+  guard $ clause.literal.is_pos (given^.c^.get_lit given_i),
   other ← rb_map.values active,
-  guard $ ¬given↣sc↣in_sos ∨ ¬other↣sc↣in_sos,
-  other_i ← other↣selected,
-  guard $ clause.literal.is_neg (other↣c↣get_lit other_i),
+  guard $ ¬given^.sc^.in_sos ∨ ¬other^.sc^.in_sos,
+  other_i ← other^.selected,
+  guard $ clause.literal.is_neg (other^.c^.get_lit other_i),
   [maybe_add_resolvent gt given other given_i other_i]
 
 @[super.inf]
diff --git a/library/tools/super/selection.lean b/library/tools/super/selection.lean
index 87413605a6..c60f812997 100644
--- a/library/tools/super/selection.lean
+++ b/library/tools/super/selection.lean
@@ -9,25 +9,25 @@ namespace super
 
 meta def simple_selection_strategy (f : (expr → expr → bool) → clause → list ℕ) : selection_strategy :=
 take dc, do gt ← get_term_order, return $
-         if dc↣selected↣empty ∧ dc↣c↣num_lits > 0
-         then { dc with selected := f gt dc↣c }
+         if dc^.selected^.empty ∧ dc^.c^.num_lits > 0
+         then { dc with selected := f gt dc^.c }
          else dc
 
 meta def dumb_selection : selection_strategy :=
 simple_selection_strategy $ λgt c,
-match c↣lits_where clause.literal.is_neg with
-| [] := list.range c↣num_lits
+match c^.lits_where clause.literal.is_neg with
+| [] := list.range c^.num_lits
 | neg_lit::_ := [neg_lit]
 end
 
 meta def selection21 : selection_strategy :=
 simple_selection_strategy $ λgt c,
 let maximal_lits := list.filter_maximal (λi j,
-  gt (c↣get_lit i)↣formula (c↣get_lit j)↣formula) (list.range c↣num_lits) in
+  gt (c^.get_lit i)^.formula (c^.get_lit j)^.formula) (list.range c^.num_lits) in
 if list.length maximal_lits = 1 then maximal_lits else
-let neg_lits := list.filter (λi, (c↣get_lit i)↣is_neg) (list.range c↣num_lits),
+let neg_lits := list.filter (λi, (c^.get_lit i)^.is_neg) (list.range c^.num_lits),
     maximal_neg_lits := list.filter_maximal (λi j,
-      gt (c↣get_lit i)↣formula (c↣get_lit j)↣formula) neg_lits in
+      gt (c^.get_lit i)^.formula (c^.get_lit j)^.formula) neg_lits in
 if ¬maximal_neg_lits^.empty then
   list.taken 1 maximal_neg_lits
 else
@@ -36,20 +36,20 @@ else
 meta def selection22 : selection_strategy :=
 simple_selection_strategy $ λgt c,
 let maximal_lits := list.filter_maximal (λi j,
-  gt (c↣get_lit i)↣formula (c↣get_lit j)↣formula) (list.range c↣num_lits),
-  maximal_lits_neg := list.filter (λi, (c↣get_lit i)↣is_neg) maximal_lits in
+  gt (c^.get_lit i)^.formula (c^.get_lit j)^.formula) (list.range c^.num_lits),
+  maximal_lits_neg := list.filter (λi, (c^.get_lit i)^.is_neg) maximal_lits in
 if ¬maximal_lits_neg^.empty then
   list.taken 1 maximal_lits_neg
 else
   maximal_lits
 
 meta def clause_weight (c : derived_clause) : nat :=
-(c↣c↣get_lits↣for (λl, expr_size l↣formula + if l↣is_pos then 10 else 1))↣sum
+(c^.c^.get_lits^.for (λl, expr_size l^.formula + if l^.is_pos then 10 else 1))^.sum
 
 meta def find_minimal_by (passive : rb_map clause_id derived_clause)
                          {A} [has_ordering A]
                          (f : derived_clause → A) : clause_id :=
-match rb_map.min $ rb_map.of_list $ passive↣values↣for $ λc, (f c, c↣id) with
+match rb_map.min $ rb_map.of_list $ passive^.values^.for $ λc, (f c, c^.id) with
 | some id := id
 | none := nat.zero
 end
@@ -59,16 +59,16 @@ meta def age_of_clause_id : name → ℕ
 | _ := 0
 
 meta def find_minimal_weight (passive : rb_map clause_id derived_clause) : clause_id :=
-find_minimal_by passive $ λc, (c↣sc↣priority, clause_weight c + c↣sc↣cost, c↣sc↣age, c↣id)
+find_minimal_by passive $ λc, (c^.sc^.priority, clause_weight c + c^.sc^.cost, c^.sc^.age, c^.id)
 
 meta def find_minimal_age (passive : rb_map clause_id derived_clause) : clause_id :=
-find_minimal_by passive $ λc, (c↣sc↣priority, c↣sc↣age, c↣id)
+find_minimal_by passive $ λc, (c^.sc^.priority, c^.sc^.age, c^.id)
 
 meta def weight_clause_selection : clause_selection_strategy :=
-take iter, do state ← state_t.read, return $ find_minimal_weight state↣passive
+take iter, do state ← state_t.read, return $ find_minimal_weight state^.passive
 
 meta def oldest_clause_selection : clause_selection_strategy :=
-take iter, do state ← state_t.read, return $ find_minimal_age state↣passive
+take iter, do state ← state_t.read, return $ find_minimal_age state^.passive
 
 meta def age_weight_clause_selection (thr mod : ℕ) : clause_selection_strategy :=
 take iter, if iter % mod < thr then
diff --git a/library/tools/super/simp.lean b/library/tools/super/simp.lean
index 45d35ebcc5..582c618ceb 100644
--- a/library/tools/super/simp.lean
+++ b/library/tools/super/simp.lean
@@ -17,7 +17,7 @@ meta def simplify_capturing_assumptions (type : expr) : tactic (expr × expr ×
 (type', heq) ← simplify default_simplify_config [] type,
 hyps ← return $ contained_lconsts type,
 hyps' ← return $ contained_lconsts_list [type', heq],
-add_hyps ← return $ list.filter (λn : expr, ¬hyps↣contains n↣local_uniq_name) hyps'↣values,
+add_hyps ← return $ list.filter (λn : expr, ¬hyps^.contains n^.local_uniq_name) hyps'^.values,
 return (type', heq, add_hyps)
 
 meta def try_simplify_left (c : clause) (i : ℕ) : tactic (list clause) :=
@@ -29,7 +29,7 @@ on_left_at c i $ λtype, do
 
 meta def try_simplify_right (c : clause) (i : ℕ) : tactic (list clause) :=
 on_right_at' c i $ λhyp, do
-  (type', heq, add_hyps) ← simplify_capturing_assumptions hyp↣local_type,
+  (type', heq, add_hyps) ← simplify_capturing_assumptions hyp^.local_type,
   heqtype ← infer_type heq,
   heqsymm ← mk_app ``eq.symm [heq],
   prf  ← mk_app ``eq.mpr [heqsymm, hyp],
@@ -38,7 +38,7 @@ on_right_at' c i $ λhyp, do
 @[super.inf]
 meta def simp_inf : inf_decl := inf_decl.mk 40 $ take given, sequence' $ do
 r ← [try_simplify_right, try_simplify_left],
-i ← list.range given↣c↣num_lits,
-[inf_if_successful 2 given (r given↣c i)]
+i ← list.range given^.c^.num_lits,
+[inf_if_successful 2 given (r given^.c i)]
 
 end super
diff --git a/library/tools/super/splitting.lean b/library/tools/super/splitting.lean
index 4220fe1efc..ccca05ada8 100644
--- a/library/tools/super/splitting.lean
+++ b/library/tools/super/splitting.lean
@@ -11,57 +11,57 @@ namespace super
 private meta def find_components : list expr → list (list (expr × ℕ)) → list (list (expr × ℕ))
 | (e::es) comps :=
   let (contain_e, do_not_contain_e) :=
-      partition (λc : list (expr × ℕ), c↣exists_ $ λf,
-        (abstract_local f↣1 e↣local_uniq_name)↣has_var) comps in
+      partition (λc : list (expr × ℕ), c^.exists_ $ λf,
+        (abstract_local f.1 e^.local_uniq_name)^.has_var) comps in
     find_components es $ list.join contain_e :: do_not_contain_e
 | _ comps := comps
 
 meta def get_components (hs : list expr) : list (list expr) :=
-(find_components hs (hs↣zip_with_index↣for $ λh, [h]))↣for $ λc,
-(sort_on (λh : expr × ℕ, h↣2) c)↣for $ λh, h↣1
+(find_components hs (hs^.zip_with_index^.for $ λh, [h]))^.for $ λc,
+(sort_on (λh : expr × ℕ, h.2) c)^.for $ λh, h.1
 
 meta def extract_assertions : clause → prover (clause × list expr) | c :=
-if c↣num_lits = 0 then return (c, [])
-else if c↣num_quants ≠ 0 then do
-  qf ← ♯ c↣open_constn c↣num_quants,
-  qf_wo_as ← extract_assertions qf↣1,
-  return (qf_wo_as↣1↣close_constn qf↣2, qf_wo_as↣2)
+if c^.num_lits = 0 then return (c, [])
+else if c^.num_quants ≠ 0 then do
+  qf ← ♯ c^.open_constn c^.num_quants,
+  qf_wo_as ← extract_assertions qf.1,
+  return (qf_wo_as.1^.close_constn qf.2, qf_wo_as.2)
 else do
-  hd ← return $ c↣get_lit 0,
-  hyp_opt ← get_sat_hyp_core hd↣formula hd↣is_neg,
+  hd ← return $ c^.get_lit 0,
+  hyp_opt ← get_sat_hyp_core hd^.formula hd^.is_neg,
   match hyp_opt with
   | some h := do
-      wo_as ← extract_assertions (c↣inst h),
-      return (wo_as↣1, h :: wo_as↣2)
+      wo_as ← extract_assertions (c^.inst h),
+      return (wo_as.1, h :: wo_as.2)
   | _ := do
-      op ← ♯c↣open_const,
-      op_wo_as ← extract_assertions op↣1,
-      return (op_wo_as↣1↣close_const op↣2, op_wo_as↣2)
+      op ← ♯c^.open_const,
+      op_wo_as ← extract_assertions op.1,
+      return (op_wo_as.1^.close_const op.2, op_wo_as.2)
   end
 
 meta def mk_splitting_clause' (empty_clause : clause) : list (list expr) → tactic (list expr × expr)
-| [] := return ([], empty_clause↣proof)
-| ([p] :: comps) := do p' ← mk_splitting_clause' comps, return (p::p'↣1, p'↣2)
+| [] := return ([], empty_clause^.proof)
+| ([p] :: comps) := do p' ← mk_splitting_clause' comps, return (p::p'.1, p'.2)
 | (comp :: comps) := do
   (hs, p') ← mk_splitting_clause' comps,
-  hnc ← mk_local_def `hnc (imp (pis comp empty_clause↣local_false) empty_clause↣local_false),
+  hnc ← mk_local_def `hnc (imp (pis comp empty_clause^.local_false) empty_clause^.local_false),
   p'' ← return $ app hnc (lambdas comp p'),
   return (hnc::hs, p'')
 
 meta def mk_splitting_clause (empty_clause : clause) (comps : list (list expr)) : tactic clause := do
 (hs, p) ← mk_splitting_clause' empty_clause comps,
-return $ { empty_clause with proof := p }↣close_constn hs
+return $ { empty_clause with proof := p }^.close_constn hs
 
 @[super.inf]
 meta def splitting_inf : inf_decl := inf_decl.mk 30 $ take given, do
-lf ← flip monad.lift state_t.read $ λst, st↣local_false,
-op ← ♯ given↣c↣open_constn given↣c↣num_binders,
-if list.bor (given↣c↣get_lits↣for $ λl, (is_local_not lf l↣formula)↣is_some) then return () else
-let comps := get_components op↣2 in
-if comps↣length < 2 then return () else do
-splitting_clause ← ♯ mk_splitting_clause op↣1 comps,
+lf ← flip monad.lift state_t.read $ λst, st^.local_false,
+op ← ♯ given^.c^.open_constn given^.c^.num_binders,
+if list.bor (given^.c^.get_lits^.for $ λl, (is_local_not lf l^.formula)^.is_some) then return () else
+let comps := get_components op.2 in
+if comps^.length < 2 then return () else do
+splitting_clause ← ♯ mk_splitting_clause op.1 comps,
 ass ← collect_ass_hyps splitting_clause,
-add_sat_clause (splitting_clause↣close_constn ass) given↣sc↣sched_default,
-remove_redundant given↣id []
+add_sat_clause (splitting_clause^.close_constn ass) given^.sc^.sched_default,
+remove_redundant given^.id []
 
 end super
diff --git a/library/tools/super/subsumption.lean b/library/tools/super/subsumption.lean
index f1667d4a3d..1c370e69b9 100644
--- a/library/tools/super/subsumption.lean
+++ b/library/tools/super/subsumption.lean
@@ -11,29 +11,29 @@ namespace super
 private meta def try_subsume_core : list clause.literal → list clause.literal → tactic unit
 | [] _ := skip
 | small large := first $ do
-  i ← small↣zip_with_index, j ← large↣zip_with_index,
+  i ← small^.zip_with_index, j ← large^.zip_with_index,
   return $ do
     unify_lit i.1 j.1,
-    try_subsume_core (small↣remove_nth i.2) (large↣remove_nth j.2)
+    try_subsume_core (small^.remove_nth i.2) (large^.remove_nth j.2)
 
 -- FIXME: this is incorrect if a quantifier is unused
 meta def try_subsume (small large : clause) : tactic unit := do
 small_open ← clause.open_metan small (clause.num_quants small),
 large_open ← clause.open_constn large (clause.num_quants large),
-guard $ small↣num_lits ≤ large↣num_lits,
-try_subsume_core small_open↣1↣get_lits large_open↣1↣get_lits
+guard $ small^.num_lits ≤ large^.num_lits,
+try_subsume_core small_open.1^.get_lits large_open.1^.get_lits
 
 meta def does_subsume (small large : clause) : tactic bool :=
 (try_subsume small large >> return tt) <|> return ff
 
 meta def does_subsume_with_assertions (small large : derived_clause) : prover bool := do
-if small↣assertions↣subset_of large↣assertions then do
-  ♯ does_subsume small↣c large↣c
+if small^.assertions^.subset_of large^.assertions then do
+  ♯ does_subsume small^.c large^.c
 else
   return ff
 
 meta def any_tt {m : Type → Type} [monad m] (active : rb_map clause_id derived_clause) (pred : derived_clause → m bool) : m bool :=
-active↣fold (return ff) $ λk a cont, do
+active^.fold (return ff) $ λk a cont, do
   v ← pred a, if v then return tt else cont
 
 meta def any_tt_list {m : Type → Type} [monad m] {A} (pred : A → m bool) : list A → m bool
@@ -43,19 +43,19 @@ meta def any_tt_list {m : Type → Type} [monad m] {A} (pred : A → m bool) : l
 @[super.inf]
 meta def forward_subsumption : inf_decl := inf_decl.mk 20 $
 take given, do active ← get_active,
-sequence' $ do a ← active↣values,
-  guard $ a↣id ≠ given↣id,
+sequence' $ do a ← active^.values,
+  guard $ a^.id ≠ given^.id,
   return $ do
-    ss ← ♯ does_subsume a↣c given↣c,
+    ss ← ♯ does_subsume a^.c given^.c,
     if ss
-    then remove_redundant given↣id [a]
+    then remove_redundant given^.id [a]
     else return ()
 
 meta def forward_subsumption_pre : prover unit := preprocessing_rule $ λnew, do
 active ← get_active, filter (λn, do
   do ss ← any_tt active (λa,
-        if a↣assertions↣subset_of n↣assertions then do
-          ♯ does_subsume a↣c n↣c
+        if a^.assertions^.subset_of n^.assertions then do
+          ♯ does_subsume a^.c n^.c
         else
           -- TODO: move to locked
           return ff),
@@ -76,7 +76,7 @@ meta def subsumption_interreduction : list derived_clause → prover (list deriv
 
 meta def subsumption_interreduction_pre : prover unit :=
 preprocessing_rule $ λnew,
-let new' := list.sort_on (λc : derived_clause, c↣c↣num_lits) new in
+let new' := list.sort_on (λc : derived_clause, c^.c^.num_lits) new in
 subsumption_interreduction new'
 
 meta def keys_where_tt {m} {K V : Type} [monad m] (active : rb_map K V) (pred : V → m bool) : m (list K) :=
@@ -86,7 +86,7 @@ meta def keys_where_tt {m} {K V : Type} [monad m] (active : rb_map K V) (pred :
 @[super.inf]
 meta def backward_subsumption : inf_decl := inf_decl.mk 20 $ λgiven, do
 active ← get_active,
-ss ← ♯ keys_where_tt active (λa, does_subsume given↣c a↣c),
-sequence' $ do id ← ss, guard (id ≠ given↣id), [remove_redundant id [given]]
+ss ← ♯ keys_where_tt active (λa, does_subsume given^.c a^.c),
+sequence' $ do id ← ss, guard (id ≠ given^.id), [remove_redundant id [given]]
 
 end super
diff --git a/library/tools/super/superposition.lean b/library/tools/super/superposition.lean
index e84f4034f6..0115ca6da8 100644
--- a/library/tools/super/superposition.lean
+++ b/library/tools/super/superposition.lean
@@ -11,8 +11,8 @@ namespace super
 meta def get_rwr_positions : expr → list (list ℕ)
 | (app a b) := [[]] ++
   do arg ← list.zip_with_index (get_app_args (app a b)),
-     pos ← get_rwr_positions arg↣1,
-     [arg↣2 :: pos]
+     pos ← get_rwr_positions arg.1,
+     [arg.2 :: pos]
 | (var _) := []
 | e := [[]]
 
@@ -27,8 +27,8 @@ end
 meta def replace_position (v : expr) : expr → list ℕ → expr
 | (app a b) (p::ps) :=
 let args := get_app_args (app a b) in
-match args↣nth p with
-| some arg := app_of_list a↣get_app_fn $ args↣update_nth p $ replace_position arg ps
+match args^.nth p with
+| some arg := app_of_list a^.get_app_fn $ args^.update_nth p $ replace_position arg ps
 | none := app a b
 end
 | e [] := v
@@ -43,7 +43,7 @@ variable ltr : bool
 variable congr_ax : name
 
 lemma {u v w} sup_ltr (F : Type u) (A : Type v) (a1 a2) (f : A → Type w) : (f a1 → F) → f a2 → a1 = a2 → F :=
-take hnfa1 hfa2 heq, hnfa1 (@eq.rec A a2 f hfa2 a1 heq↣symm)
+take hnfa1 hfa2 heq, hnfa1 (@eq.rec A a2 f hfa2 a1 heq^.symm)
 lemma {u v w} sup_rtl (F : Type u) (A : Type v) (a1 a2) (f : A → Type w) : (f a1 → F) → f a2 → a2 = a1 → F :=
 take hnfa1 hfa2 heq, hnfa1 (@eq.rec A a2 f hfa2 a1 heq)
 
@@ -54,11 +54,11 @@ match is_eq e with
 end
 
 meta def try_sup : tactic clause := do
-guard $ (c1↣get_lit i1)↣is_pos,
-qf1 ← c1↣open_metan c1↣num_quants,
-qf2 ← c2↣open_metan c2↣num_quants,
-(rwr_from, rwr_to) ← (is_eq_dir (qf1↣1↣get_lit i1)↣formula ltr)↣to_monad,
-atom ← return (qf2↣1↣get_lit i2)↣formula,
+guard $ (c1^.get_lit i1)^.is_pos,
+qf1 ← c1^.open_metan c1^.num_quants,
+qf2 ← c2^.open_metan c2^.num_quants,
+(rwr_from, rwr_to) ← (is_eq_dir (qf1.1^.get_lit i1)^.formula ltr)^.to_monad,
+atom ← return (qf2.1^.get_lit i2)^.formula,
 eq_type ← infer_type rwr_from,
 atom_at_pos_type ← infer_type $ get_position atom pos,
 unify eq_type atom_at_pos_type,
@@ -69,52 +69,52 @@ guard $ ¬gt rwr_to' rwr_from',
 rwr_ctx_varn ← mk_fresh_name,
 abs_rwr_ctx ← return $
   lam rwr_ctx_varn binder_info.default eq_type
-  (if (qf2↣1↣get_lit i2)↣is_neg
+  (if (qf2.1^.get_lit i2)^.is_neg
    then replace_position (mk_var 0) atom pos
-   else imp (replace_position (mk_var 0) atom pos) c2↣local_false),
-lf_univ ← infer_univ c1↣local_false,
+   else imp (replace_position (mk_var 0) atom pos) c2^.local_false),
+lf_univ ← infer_univ c1^.local_false,
 univ ← infer_univ eq_type,
 atom_univ ← infer_univ atom,
-op1 ← qf1↣1↣open_constn i1,
-op2 ← qf2↣1↣open_constn c2↣num_lits,
-hi2 ← (op2↣2↣nth i2)↣to_monad,
+op1 ← qf1.1^.open_constn i1,
+op2 ← qf2.1^.open_constn c2^.num_lits,
+hi2 ← (op2.2^.nth i2)^.to_monad,
 new_atom ← whnf $ app abs_rwr_ctx rwr_to',
-new_hi2 ← return $ local_const hi2↣local_uniq_name `H binder_info.default new_atom,
+new_hi2 ← return $ local_const hi2^.local_uniq_name `H binder_info.default new_atom,
 new_fin_prf ←
-  return $ app_of_list (const congr_ax [lf_univ, univ, atom_univ]) [c1↣local_false, eq_type, rwr_from, rwr_to,
-            abs_rwr_ctx, (op2↣1↣close_const hi2)↣proof, new_hi2],
-clause.meta_closure (qf1↣2 ++ qf2↣2) $ (op1↣1↣inst new_fin_prf)↣close_constn (op1↣2 ++ op2↣2↣update_nth i2 new_hi2)
+  return $ app_of_list (const congr_ax [lf_univ, univ, atom_univ]) [c1^.local_false, eq_type, rwr_from, rwr_to,
+            abs_rwr_ctx, (op2.1^.close_const hi2)^.proof, new_hi2],
+clause.meta_closure (qf1.2 ++ qf2.2) $ (op1.1^.inst new_fin_prf)^.close_constn (op1.2 ++ op2.2^.update_nth i2 new_hi2)
 
 meta def rwr_positions (c : clause) (i : nat) : list (list ℕ) :=
-get_rwr_positions (c↣get_lit i)↣formula
+get_rwr_positions (c^.get_lit i)^.formula
 
 meta def try_add_sup : prover unit :=
-(do c' ← ♯ try_sup gt ac1↣c ac2↣c i1 i2 pos ltr congr_ax,
-    inf_score 2 [ac1↣sc, ac2↣sc] >>= mk_derived c' >>= add_inferred)
+(do c' ← ♯ try_sup gt ac1^.c ac2^.c i1 i2 pos ltr congr_ax,
+    inf_score 2 [ac1^.sc, ac2^.sc] >>= mk_derived c' >>= add_inferred)
   <|> return ()
 
 meta def superposition_back_inf : inference :=
 take given, do active ← get_active, sequence' $ do
-  given_i ← given↣selected,
-  guard (given↣c↣get_lit given_i)↣is_pos,
-  option.to_monad $ is_eq (given↣c↣get_lit given_i)↣formula,
+  given_i ← given^.selected,
+  guard (given^.c^.get_lit given_i)^.is_pos,
+  option.to_monad $ is_eq (given^.c^.get_lit given_i)^.formula,
   other ← rb_map.values active,
-  guard $ ¬given↣sc↣in_sos ∨ ¬other↣sc↣in_sos,
-  other_i ← other↣selected,
-  pos ← rwr_positions other↣c other_i,
+  guard $ ¬given^.sc^.in_sos ∨ ¬other^.sc^.in_sos,
+  other_i ← other^.selected,
+  pos ← rwr_positions other^.c other_i,
   -- FIXME(gabriel): ``sup_ltr fails to resolve at runtime
   [do try_add_sup gt given other given_i other_i pos tt ``super.sup_ltr,
       try_add_sup gt given other given_i other_i pos ff ``super.sup_rtl]
 
 meta def superposition_fwd_inf : inference :=
 take given, do active ← get_active, sequence' $ do
-  given_i ← given↣selected,
+  given_i ← given^.selected,
   other ← rb_map.values active,
-  guard $ ¬given↣sc↣in_sos ∨ ¬other↣sc↣in_sos,
-  other_i ← other↣selected,
-  guard (other↣c↣get_lit other_i)↣is_pos,
-  option.to_monad $ is_eq (other↣c↣get_lit other_i)↣formula,
-  pos ← rwr_positions given↣c given_i,
+  guard $ ¬given^.sc^.in_sos ∨ ¬other^.sc^.in_sos,
+  other_i ← other^.selected,
+  guard (other^.c^.get_lit other_i)^.is_pos,
+  option.to_monad $ is_eq (other^.c^.get_lit other_i)^.formula,
+  pos ← rwr_positions given^.c given_i,
   [do try_add_sup gt other given other_i given_i pos tt ``super.sup_ltr,
       try_add_sup gt other given other_i given_i pos ff ``super.sup_rtl]
 
diff --git a/library/tools/super/utils.lean b/library/tools/super/utils.lean
index 1bee92bf2a..665f1c91b0 100644
--- a/library/tools/super/utils.lean
+++ b/library/tools/super/utils.lean
@@ -60,10 +60,10 @@ def exists_ {A} (l : list A) (p : A → Prop) [decidable_pred p] : bool :=
 list.any l (λx, to_bool (p x))
 
 def subset_of {A} [decidable_eq A] (xs ys : list A) :=
-xs↣for_all (λx, x ∈ ys)
+xs^.for_all (λx, x ∈ ys)
 
 def filter_maximal {A} (gt : A → A → bool) (l : list A) : list A :=
-filter (λx, l↣for_all (λy, ¬gt y x)) l
+filter (λx, l^.for_all (λy, ¬gt y x)) l
 
 private def zip_with_index' {A} : ℕ → list A → list (A × ℕ)
 | _ nil := nil