chore(frontends/lean/builtin_exprs): remove support for (<infix>) and (<infix> <expr>) notations

In Lean 4, we will support the more general

`a + ·` ==> `fun x, a + x`
`· + b` ==> `fun x, x + b`
`· + ·` ==> `fun x y, x + y`
`f · y` ==> `fun x, f a y`
`g · · b` ==> `fun x y, g x y b`

library/init/control/monad.lean

@@ -23,7 +23,7 @@ infixr >=> := mcomp
 
 class Monad (m : Type u → Type v) extends Applicative m, HasBind m : Type (max (u+1) v) :=
 (map      := λ α β f x, x >>= pure ∘ f)
-(seq      := λ α β f x, f >>= (<$> x))
+(seq      := λ α β f x, f >>= (λ y, y <$> x))
 (seqLeft  := λ α β x y, x >>= λ a, y >>= λ _, pure a)
 (seqRight := λ α β x y, x >>= λ _, y)
 

library/init/data/array/basic.lean

@@ -354,7 +354,7 @@ else
   false
 
 instance [HasBeq α] : HasBeq (Array α) :=
-⟨λ a b, isEqv a b (==)⟩
+⟨λ a b, isEqv a b HasBeq.beq⟩
 
 -- TODO(Leo): justify termination using wf-rec, and use `fswap`
 partial def reverseAux : Array α → Nat → Array α

library/init/data/list/basic.lean

@@ -71,7 +71,7 @@ theorem appendAssoc : ∀ (as bs cs : List α), (as ++ bs) ++ cs = as ++ (bs ++
 | []      bs cs := rfl
 | (a::as) bs cs :=
   show ((a::as) ++ bs) ++ cs = (a::as) ++ (bs ++ cs),      from
-  have h₁ : ((a::as) ++ bs) ++ cs = a::(as++bs) ++ cs,     from congrArg (++ cs) (consAppend a as bs),
+  have h₁ : ((a::as) ++ bs) ++ cs = a::(as++bs) ++ cs,     from congrArg (λ ds, ds ++ cs) (consAppend a as bs),
   have h₂ : a::(as++bs) ++ cs     = a::((as++bs) ++ cs),   from consAppend a (as++bs) cs,
   have h₃ : a::((as++bs) ++ cs)   = a::(as ++ (bs ++ cs)), from congrArg (λ as, a::as) (appendAssoc as bs cs),
   have h₄ : a::(as ++ (bs ++ cs)) = (a::as ++ (bs ++ cs)), from (consAppend a as (bs++cs)).symm,
@@ -325,7 +325,7 @@ inductive Less [HasLess α] : List α → List α → Prop
 instance [HasLess α] : HasLess (List α) :=
 ⟨List.Less⟩
 
-instance hasDecidableLt [HasLess α] [h : DecidableRel ((<) : α → α → Prop)] : Π l₁ l₂ : List α, Decidable (l₁ < l₂)
+instance hasDecidableLt [HasLess α] [h : DecidableRel HasLess.Less] : Π l₁ l₂ : List α, Decidable (l₁ < l₂)
 | []      []      := isFalse (λ h, match h with end)
 | []      (b::bs) := isTrue (Less.nil _ _)
 | (a::as) []      := isFalse (λ h, match h with end)
@@ -350,7 +350,7 @@ instance hasDecidableLt [HasLess α] [h : DecidableRel ((<) : α → α → Prop
 instance [HasLess α] : HasLessEq (List α) :=
 ⟨List.LessEq⟩
 
-instance hasDecidableLe [HasLess α] [h : DecidableRel ((<) : α → α → Prop)] : Π l₁ l₂ : List α, Decidable (l₁ ≤ l₂) :=
+instance hasDecidableLe [HasLess α] [h : DecidableRel (HasLess.Less : α → α → Prop)] : Π l₁ l₂ : List α, Decidable (l₁ ≤ l₂) :=
 λ a b, Not.Decidable
 
 /--  `isPrefixOf l₁ l₂` returns `true` Iff `l₁` is a prefix of `l₂`. -/

library/init/data/nat/basic.lean

@@ -466,7 +466,7 @@ protected theorem addLeAddRight {n m : Nat} (h : n ≤ m) (k : Nat) : n + k ≤
 have h₁ : n + k = k + n, from Nat.addComm _ _,
 have h₂ : k + n ≤ k + m, from Nat.addLeAddLeft h k,
 have h₃ : k + m = m + k, from Nat.addComm _ _,
-transRelLeft (≤) (transRelRight (≤) h₁ h₂) h₃
+transRelLeft (λ a b, a ≤ b) (transRelRight (λ a b, a ≤ b) h₁ h₂) h₃
 
 protected theorem addLtAddLeft {n m : Nat} (h : n < m) (k : Nat) : k + n < k + m :=
 ltOfSuccLe (addSucc k n ▸ Nat.addLeAddLeft (succLeOfLt h) k)
@@ -509,7 +509,7 @@ protected theorem zeroLtBit0 : ∀ {n : Nat}, n ≠ 0 → 0 < bit0 n
 | (succ n) h :=
   have h₁ : 0 < succ (succ (bit0 n)),             from zeroLtSucc _,
   have h₂ : succ (succ (bit0 n)) = bit0 (succ n), from (Nat.bit0SuccEq n).symm,
-  transRelLeft (<) h₁ h₂
+  transRelLeft (λ a b, a < b) h₁ h₂
 
 protected theorem zeroLtBit1 (n : Nat) : 0 < bit1 n :=
 zeroLtSucc _
@@ -573,7 +573,7 @@ protected theorem bit0Inj : ∀ {n m : Nat}, bit0 n = bit0 m → n = m
   have succ (n + n) = succ (m + m), from this,
   have n + n = m + m, from Nat.noConfusion this id,
   have n = m, from bit0Inj this,
-  congrArg (+1) this
+  congrArg (λ a, a + 1) this
 
 protected theorem bit1Inj : ∀ {n m : Nat}, bit1 n = bit1 m → n = m :=
 λ n m h,

library/init/data/option/basic.lean

@@ -85,4 +85,4 @@ instance {α : Type u} [DecidableEq α] : DecidableEq (Option α) :=
    | (isTrue e)  := isTrue (congrArg (@some α) e)
    | (isFalse n) := isFalse (λ h, Option.noConfusion h (λ e, absurd e n))}
 
-instance {α : Type u} [HasLess α] : HasLess (Option α) := ⟨Option.lt (<)⟩
+instance {α : Type u} [HasLess α] : HasLess (Option α) := ⟨Option.lt HasLess.Less⟩

library/init/data/ordering/basic.lean

@@ -36,8 +36,8 @@ if lt a b      then Ordering.lt
 else if lt b a then Ordering.gt
 else                Ordering.Eq
 
-def cmp {α : Type u} [HasLess α] [DecidableRel ((<) : α → α → Prop)] (a b : α) : Ordering :=
-cmpUsing (<) a b
+def cmp {α : Type u} [HasLess α] [DecidableRel (HasLess.Less : α → α → Prop)] (a b : α) : Ordering :=
+cmpUsing HasLess.Less a b
 
 instance : DecidableEq Ordering :=
 {decEq := λ a b,

library/init/data/string/basic.lean

@@ -295,7 +295,7 @@ anyAux s s.bsize p 0
 !s.any (λ c, !p c)
 
 def contains (s : String) (c : Char) : Bool :=
-s.any (== c)
+s.any (λ a, a == c)
 
 @[specialize] partial def mapAux (f : Char → Char) : Pos → String → String
 | i s :=
@@ -412,7 +412,7 @@ match s with
 !s.any (λ c, !p c)
 
 def contains (s : Substring) (c : Char) : Bool :=
-s.any (== c)
+s.any (λ a, a == c)
 
 @[specialize] partial def takeWhileAux (s : String) (stopPos : String.Pos) (p : Char → Bool) : String.Pos → String.Pos
 | i :=

library/init/lean/compiler/constfolding.lean

@@ -63,10 +63,10 @@ do n₁   ← getNumLit a₁;
    info ← getInfoFromVal a₁;
    pure $ mkUIntLit info (fn info beforeErasure n₁ n₂)
 
-def foldUIntAdd := foldBinUInt $ λ _ _, (+)
-def foldUIntMul := foldBinUInt $ λ _ _, (*)
-def foldUIntDiv := foldBinUInt $ λ _ _, (/)
-def foldUIntMod := foldBinUInt $ λ _ _, (%)
+def foldUIntAdd := foldBinUInt $ λ _ _, HasAdd.add
+def foldUIntMul := foldBinUInt $ λ _ _, HasMul.mul
+def foldUIntDiv := foldBinUInt $ λ _ _, HasDiv.div
+def foldUIntMod := foldBinUInt $ λ _ _, HasMod.mod
 def foldUIntSub := foldBinUInt $ λ info _ a b, (a + (info.size - b))
 
 def preUIntBinFoldFns : List (Name × BinFoldFn) :=
@@ -81,11 +81,11 @@ do n₁   ← getNumLit a₁;
    n₂   ← getNumLit a₂;
    pure $ Expr.lit (Literal.natVal (fn n₁ n₂))
 
-def foldNatAdd (_ : Bool) := foldNatBinOp (+)
-def foldNatMul (_ : Bool) := foldNatBinOp (*)
-def foldNatDiv (_ : Bool) := foldNatBinOp (/)
-def foldNatMod (_ : Bool) := foldNatBinOp (%)
-def foldNatPow (_ : Bool) := foldNatBinOp (^)
+def foldNatAdd (_ : Bool) := foldNatBinOp HasAdd.add
+def foldNatMul (_ : Bool) := foldNatBinOp HasMul.mul
+def foldNatDiv (_ : Bool) := foldNatBinOp HasDiv.div
+def foldNatMod (_ : Bool) := foldNatBinOp HasMod.mod
+def foldNatPow (_ : Bool) := foldNatBinOp HasPow.pow
 
 def mkNatEq (a b : Expr) : Expr :=
 mkBinApp (Expr.app (Expr.const `Eq [Level.one]) (Expr.const `Nat [])) a b

library/init/lean/compiler/externattr.lean

@@ -122,7 +122,7 @@ def expandExternPattern (pattern : String) (args : List String) : String :=
 expandExternPatternAux args pattern.length pattern.mkIterator ""
 
 def mkSimpleFnCall (fn : String) (args : List String) : String :=
-fn ++ "(" ++ ((args.intersperse ", ").foldl (++) "") ++ ")"
+fn ++ "(" ++ ((args.intersperse ", ").foldl HasAppend.append "") ++ ")"
 
 def expandExternEntry : ExternEntry → List String → Option String
 | (ExternEntry.adhoc _) args        := none -- backend must expand it

library/init/lean/compiler/ir/boxing.lean

@@ -36,7 +36,7 @@ abbrev N := State Nat
 
 private def mkFresh : N VarId :=
 do idx ← get;
-   modify (+1);
+   modify (λ n, n + 1);
    pure {idx := idx }
 
 def requiresBoxedVersion (env : Environment) (decl : Decl) : Bool :=
@@ -111,7 +111,7 @@ structure BoxingContext :=
 abbrev M := ReaderT BoxingContext (StateT Index Id)
 
 def mkFresh : M VarId :=
-do idx ← getModify (+1);
+do idx ← getModify (λ n, n + 1);
    pure { idx := idx }
 
 def getEnv : M Environment := BoxingContext.env <$> read

library/init/lean/compiler/ir/checker.lean

@@ -76,13 +76,13 @@ def checkExpr (ty : IRType) : Expr → M Unit
 | (Expr.ctor c ys)          := when c.isRef (checkObjType ty) *> checkArgs ys
 | (Expr.reset _ x)          := checkObjVar x *> checkObjType ty
 | (Expr.reuse x i u ys)     := checkObjVar x *> checkArgs ys *> checkObjType ty
-| (Expr.box xty x)          := checkObjType ty *> checkScalarVar x *> checkVarType x (==xty)
+| (Expr.box xty x)          := checkObjType ty *> checkScalarVar x *> checkVarType x (λ t, t == xty)
 | (Expr.unbox x)            := checkScalarType ty *> checkObjVar x
 | (Expr.proj _ x)           := checkObjVar x *> checkObjType ty
-| (Expr.uproj _ x)          := checkObjVar x *> checkType ty (==IRType.usize)
+| (Expr.uproj _ x)          := checkObjVar x *> checkType ty (λ t, t == IRType.usize)
 | (Expr.sproj _ _ x)        := checkObjVar x *> checkScalarType ty
-| (Expr.isShared x)         := checkObjVar x *> checkType ty (==IRType.uint8)
-| (Expr.isTaggedPtr x)      := checkObjVar x *> checkType ty (==IRType.uint8)
+| (Expr.isShared x)         := checkObjVar x *> checkType ty (λ t, t == IRType.uint8)
+| (Expr.isTaggedPtr x)      := checkObjVar x *> checkType ty (λ t, t == IRType.uint8)
 | (Expr.lit (LitVal.str _)) := checkObjType ty
 | (Expr.lit _)              := pure ()
 

library/init/lean/compiler/ir/expandresetreuse.lean

@@ -137,7 +137,7 @@ mask.foldl
 
 abbrev M := ReaderT Context (State Nat)
 def mkFresh : M VarId :=
-do idx ← get; modify (+1); pure { idx := idx }
+do idx ← get; modify (λ n, n + 1); pure { idx := idx }
 
 def releaseUnreadFields (y : VarId) (mask : Mask) (b : FnBody) : M FnBody :=
 mask.size.mfold

library/init/lean/compiler/ir/normids.lean

@@ -80,17 +80,17 @@ abbrev N := ReaderT IndexRenaming (State Nat)
 
 @[inline] def withVar {α : Type} (x : VarId) (k : VarId → N α) : N α :=
 λ m, do
-  n ← getModify (+1);
+  n ← getModify (λ n, n + 1);
   k { idx := n } (m.insert x.idx n)
 
 @[inline] def withJP {α : Type} (x : JoinPointId) (k : JoinPointId → N α) : N α :=
 λ m, do
-  n ← getModify (+1);
+  n ← getModify (λ n, n + 1);
   k { idx := n } (m.insert x.idx n)
 
 @[inline] def withParams {α : Type} (ps : Array Param) (k : Array Param → N α) : N α :=
 λ m, do
-  m ← ps.mfoldl (λ (m : IndexRenaming) p, do n ← getModify (+1); pure $ m.insert p.x.idx n) m;
+  m ← ps.mfoldl (λ (m : IndexRenaming) p, do n ← getModify (λ n, n + 1); pure $ m.insert p.x.idx n) m;
   let ps := ps.map $ λ p, { x := normVar p.x m, .. p };
   k ps m
 

library/init/lean/compiler/ir/resetreuse.lean

@@ -59,7 +59,7 @@ private partial def S (w : VarId) (c : CtorInfo) : FnBody → FnBody
 abbrev M := ReaderT LocalContext (StateT Index Id)
 
 private def mkFresh : M VarId :=
-do idx ← getModify (+1);
+do idx ← getModify (λ n, n + 1);
    pure { idx := idx }
 
 private def tryS (x : VarId) (c : CtorInfo) (b : FnBody) : M FnBody :=

library/init/lean/format.lean

@@ -27,7 +27,7 @@ instance : HasCoe String Format := ⟨text⟩
 instance : Inhabited Format     := ⟨nil⟩
 
 def join (xs : List Format) : Format :=
-xs.foldl (++) ""
+xs.foldl HasAppend.append ""
 
 def isNil : Format → Bool
 | nil := true

library/init/lean/parser/parser.lean

@@ -417,7 +417,7 @@ partial def whitespace : BasicParserFn
     else if curr == '-' then
       let i    := input.next i;
       let curr := input.get i;
-      if curr == '-' then andthenAux (takeUntilFn (= '\n')) whitespace c (s.next input i)
+      if curr == '-' then andthenAux (takeUntilFn (λ c, c = '\n')) whitespace c (s.next input i)
       else s
     else if curr == '/' then
       let i    := input.next i;
@@ -707,7 +707,7 @@ else
     | _                 := s.mkErrorAt errorMsg startPos
 
 def symbolFnAux (sym : String) (errorMsg : String) : BasicParserFn :=
-satisfySymbolFn (== sym) errorMsg
+satisfySymbolFn (λ s, s == sym) errorMsg
 
 def insertToken (sym : String) (lbp : Option Nat) (tks : Trie TokenConfig) : ExceptT String Id (Trie TokenConfig) :=
 match tks.find sym, lbp with

library/init/wf.lean

@@ -136,7 +136,7 @@ def Nat.ltWf : WellFounded Nat.lt :=
         (λ e, Eq.substr e ih) (Acc.inv ih))⟩
 
 def measure {α : Sort u} : (α → Nat) → α → α → Prop :=
-InvImage (<)
+InvImage (λ a b, a < b)
 
 def measureWf {α : Sort u} (f : α → Nat) : WellFounded (measure f) :=
 InvImage.wf f Nat.ltWf

src/frontends/lean/builtin_exprs.cpp

@@ -755,68 +755,7 @@ expr mk_infix_function(expr const & e) {
     return mk_annotation(*g_infix_function, e);
 }
 
-/* Check whether notation such as (<) (+ 10) is applicable.
-   Like Haskell,
-     (<) is notation for (fun x y, x < y)
-     (+ 10) is notation for (fun x, x + 10)
-
-   This kind of notation is applicable when
-   1- The current token is a keyword.
-   2- There is no entry for this token in the nud table
-   3- There is an entry for this token in the led table,
-      and exactly one Expr transition to an accepting state.
-
-   If the notation is applicable, this function returns the accepting list.
-*/
-static list<notation::accepting> is_infix_paren_notation(parser & p) {
-    if (p.curr_is_keyword() &&
-        !p.nud().find(p.get_token_info().value())) {
-        list<pair<transition, parse_table>> ts = p.led().find(p.get_token_info().value());
-        if (ts && !tail(ts) && head(ts).second.is_accepting()) {
-            notation::action const & act = head(ts).first.get_action();
-            if (act.kind() == notation::action_kind::Expr) {
-                return head(ts).second.is_accepting();
-            }
-        }
-    }
-    return list<notation::accepting>();
-}
-
-static expr parse_infix_paren(parser & p, list<notation::accepting> const & accs, pos_info const & pos) {
-    expr args[2];
-    buffer<expr> vars;
-    bool fixed_second_arg = false;
-    args[0] = mk_local(p.next_name(), "_x", mk_expr_placeholder(), mk_binder_info());
-    vars.push_back(args[0]);
-    p.next();
-    if (p.curr_is_token(get_rparen_tk())) {
-        p.next();
-        args[1] = mk_local(p.next_name(), "_y", mk_expr_placeholder(), mk_binder_info());
-        vars.push_back(args[1]);
-    } else {
-        fixed_second_arg = true;
-        args[1] = p.parse_expr();
-        consume_rparen(p);
-    }
-    buffer<expr> cs;
-    for (notation::accepting const & acc : accs) {
-        expr r = p.copy_with_new_pos(acc.get_expr(), pos);
-        if (!fixed_second_arg && get_app_num_args(r) == 2 && !has_loose_bvars(app_fn(app_fn(r))) &&
-            is_var(app_arg(app_fn(r)), 1) && is_var(app_arg(r), 0)) {
-            /* r is of the form (f #1 #0).
-               Thus, we add f to cs instead of (fun x y, f x y) */
-            cs.push_back(app_fn(app_fn(r)));
-        } else {
-            r = p.save_pos(mk_infix_function(Fun(vars, instantiate_rev(r, 2, args), p)), pos);
-            cs.push_back(r);
-        }
-    }
-    return p.save_pos(mk_choice(cs.size(), cs.data()), pos);
-}
-
 static expr parse_lparen(parser & p, unsigned, expr const *, pos_info const & pos) {
-    if (auto accs = is_infix_paren_notation(p))
-        return parse_infix_paren(p, accs, pos);
     expr e = p.parse_expr();
     if (p.curr_is_token(get_comma_tk())) {
         buffer<expr> args;