chore: remove $. notation

It has been replaced by `|>.`

src/Lean/Elab/App.lean

@@ -732,9 +732,6 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
   | `($(e).$idx:fieldIdx) =>
     let idx := idx.isFieldIdx?.get!
     elabAppFn e (LVal.fieldIdx idx :: lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
-  | `($e $.$field) => do
-     let f ← `($(e).$field)
-     elabAppFn f lvals namedArgs args expectedType? explicit ellipsis overloaded acc
   | `($e |>. $field) => do
      let f ← `($(e).$field)
      elabAppFn f lvals namedArgs args expectedType? explicit ellipsis overloaded acc
@@ -857,7 +854,6 @@ private def elabAtom : TermElab := fun stx expectedType? =>
 @[builtinTermElab ident] def elabIdent : TermElab := elabAtom
 @[builtinTermElab namedPattern] def elabNamedPattern : TermElab := elabAtom
 @[builtinTermElab explicitUniv] def elabExplicitUniv : TermElab := elabAtom
-@[builtinTermElab dollarProj] def expandDollarProj : TermElab := elabAtom
 @[builtinTermElab pipeProj] def expandPipeProj : TermElab := elabAtom
 
 @[builtinTermElab explicit] def elabExplicit : TermElab := fun stx expectedType? =>

src/Lean/Parser/Term.lean

@@ -186,7 +186,6 @@ def isIdent (stx : Syntax) : Bool :=
 @[builtinTermParser] def namedPattern : TrailingParser := tparser! checkStackTop isIdent "expected preceding identifier" >> checkNoWsBefore "no space before '@'" >> "@" >> termParser maxPrec
 
 @[builtinTermParser] def dollar     := tparser!:0 atomic (" $" >> checkWsBefore "expected space") >> termParser 0
-@[builtinTermParser] def dollarProj := tparser!:0 " $. " >> (fieldIdx <|> ident) -- TODO delete
 @[builtinTermParser] def pipeProj   := tparser!:0 " |>. " >> (fieldIdx <|> ident)
 
 @[builtinTermParser] def subst := tparser!:75 " ▸ " >> sepBy1 (termParser 75) " ▸ "

tests/compiler/lazylist.lean

@@ -124,5 +124,5 @@ def main : IO Unit := do
 let n := 40;
 IO.println tst.isEmpty;
 IO.println tst.head;
-IO.println $ fib.interleave (iota.map (· + 100)) $.approx n;
-IO.println $ iota.map (· + 10) $.filter (· % 2 == 0) $.approx n
+IO.println <| fib.interleave (iota.map (· + 100)) |>.approx n;
+IO.println <| iota.map (· + 10) |>.filter (· % 2 == 0) |>.approx n

tests/lean/repr_issue.lean

@@ -1,4 +1,4 @@
-
+--
 def foo {m} [Monad m] [MonadExcept String m] [MonadState (Array Nat) m] : m Nat :=
 tryCatch
   (do modify $ fun (a : Array Nat) => a.set! 0 33;
@@ -13,5 +13,5 @@ foo
 
 -- The following examples were producing an element of Type `id (Except String Nat)`.
 -- Type class resolution was failing to produce an instance for `Repr (id (Except String Nat))` because `id` is not transparent.
-#eval ex₁.run' (mkArray 10 1000) $.run
-#eval ex₂.run' (mkArray 10 1000) $.run
+#eval ex₁.run' (mkArray 10 1000) |>.run
+#eval ex₂.run' (mkArray 10 1000) |>.run

tests/lean/run/doNotation1.lean

@@ -135,9 +135,9 @@ else
   return y+z
 
 def f1Test : IO Unit := do
-unless (← f1 30 $.run' 0) == 140 do
+unless (← f1 30 |>.run' 0) == 140 do
   throw $ IO.userError $ "error"
-unless (← f1 5 $.run' 0) == 15 do
+unless (← f1 5 |>.run' 0) == 15 do
   throw $ IO.userError $ "error"
 
 #eval f1Test

tests/lean/run/doNotation2.lean

@@ -21,13 +21,13 @@ if xs.isEmpty then
 dbgTrace! ">>> xs: {xs}"
 return xs.length
 
-#eval g [1, 2, 3] $.run' 10
-#eval g [] $.run' 10
+#eval g [1, 2, 3] |>.run' 10
+#eval g [] |>.run' 10
 
-theorem ex1 : (g [1, 2, 4, 5] $.run' 0) = 4 :=
+theorem ex1 : (g [1, 2, 4, 5] |>.run' 0) = 4 :=
 rfl
 
-theorem ex2 : (g [] $.run' 0) = 1 :=
+theorem ex2 : (g [] |>.run' 0) = 1 :=
 rfl
 
 def h (x : Nat) (y : Nat) : Nat := do

tests/lean/run/dollarProjIssue.lean

@@ -1,10 +1,8 @@
-
-
 def g (x : Nat) : List (Nat × List Nat) :=
 [(x, [x, x]), (x, [])]
 
 def h (x : Nat) : List (Nat × List Nat) :=
-g x $.filter fun ⟨_, xs⟩ => xs.isEmpty
+g x |>.filter fun ⟨_, xs⟩ => xs.isEmpty
 
 theorem ex1 : g 10 = [(10, [10, 10]), (10, [])] :=
 rfl

tests/lean/run/forBodyResultTypeIssue.lean

@@ -1,17 +1,17 @@
-abbrev M := ExceptT String $ StateT Nat Id
+abbrev M := ExceptT String <| StateT Nat Id
 
 def f (xs : List Nat) : M Unit := do
 for x in xs do
   if x == 0 then
     throw "contains zero"
 
-#eval f [1, 2, 3] $.run' 0
-#eval f [1, 0, 3] $.run' 0
+#eval f [1, 2, 3] |>.run' 0
+#eval f [1, 0, 3] |>.run' 0
 
-theorem ex1 : f [1, 2, 3] $.run' 0 = Except.ok () :=
+theorem ex1 : f [1, 2, 3] |>.run' 0 = Except.ok () :=
 rfl
 
-theorem ex2 : f [1, 0, 3] $.run' 0 = Except.error "contains zero" :=
+theorem ex2 : f [1, 0, 3] |>.run' 0 = Except.error "contains zero" :=
 rfl
 
 universes u
@@ -30,4 +30,4 @@ for x in xs do
   let a ← idM a
   checkEq x a
 
-#eval g [1, (2:Nat), 3] 1 $.run
+#eval g [1, (2:Nat), 3] 1 |>.run

tests/lean/run/frontend1.lean

@@ -154,9 +154,9 @@ f a
 #eval runM "#check #[1, 2, 3].foldl (fun r a => r.push a) #[]"
 #eval runM "#check #[1, 2, 3].foldl (fun r a => (r.push a).push a) #[]"
 #eval runM "#check #[1, 2, 3].foldl (fun r a => ((r.push a).push a).push a) #[]"
-#eval runM "#check #[].push one $.push two $.push zero $.size.succ"
-#eval runM "#check #[1, 2].foldl (fun r a => r.push a $.push a $.push a) #[]"
-#eval runM "#check #[1, 2].foldl (init := #[]) $ fun r a => r.push a $.push a"
+#eval runM "#check #[].push one |>.push two |>.push zero |>.size.succ"
+#eval runM "#check #[1, 2].foldl (fun r a => r.push a |>.push a |>.push a) #[]"
+#eval runM "#check #[1, 2].foldl (init := #[]) $ fun r a => r.push a |>.push a"
 
 #eval runM "#check let x := one + zero; x + x"
 -- set_option trace.Elab true

tests/lean/run/letrecInProofs.lean

@@ -78,12 +78,12 @@ open Tree
 
 theorem ex1 (x : Tree) : x ≠ node leaf (node x leaf) := by
   intro h
-  exact absurd rfl $ Tree.acyclic _ _ h $.2.1.2.1.1
+  exact absurd rfl $ Tree.acyclic _ _ h |>.2.1.2.1.1
 
 theorem ex2 (x : Tree) : x ≠ node x leaf := by
   intro h
-  exact absurd rfl $ Tree.acyclic _ _ h $.1.1
+  exact absurd rfl $ Tree.acyclic _ _ h |>.1.1
 
 theorem ex3 (x y : Tree) : x ≠ node y x := by
   intro h
-  exact absurd rfl $ Tree.acyclic _ _ h $.2.1.1
+  exact absurd rfl $ Tree.acyclic _ _ h |>.2.1.1

tests/lean/run/macro2.lean

@@ -7,19 +7,19 @@ end Foo
 
 syntax:60 term "+++" term:59 : term
 
-syntax "<|" term "|>" : term
+syntax "<||" term "||>" : term
 
 macro_rules
 | `($a +++ $b) => `($a + $b + $b)
 
 macro_rules
-| `(<| $x |>) => `($x +++ 1 ** 2)
+| `(<|| $x ||>) => `($x +++ 1 ** 2)
 
 
-#check <| 2 |>
+#check <|| 2 ||>
 
-#check <| ~2 |>
+#check <|| ~2 ||>
 
-#check <| ~~2 |>
+#check <|| ~~2 ||>
 
-#check <| <| 3 |> |>
+#check <|| <|| 3 ||> ||>

tests/lean/run/matchDiscrType.lean

@@ -1,10 +1,8 @@
-
-
 def g (x : Nat) : List (Nat × List Nat) :=
 [(x, [x, x]), (x, [])]
 
 def h (x : Nat) : List Nat :=
-let xs := g x $.filter (fun ⟨_, xs⟩ => xs.isEmpty)
+let xs := g x |>.filter (fun ⟨_, xs⟩ => xs.isEmpty)
 xs.map (·.1)
 
 theorem ex1 : g 10 = [(10, [10, 10]), (10, [])] :=

tests/lean/run/optParam.lean

@@ -1,12 +1,10 @@
-
-
 def p (x : Nat := 0) : Nat × Nat :=
 (x, x)
 
 theorem ex1 : p.1 = 0 :=
 rfl
 
-theorem ex2 : p (x := 1) $.2 = 1 :=
+theorem ex2 : p (x := 1) |>.2 = 1 :=
 rfl
 
 def c {α : Type} [Inhabited α] : α × α :=

tests/lean/run/stateRef.lean

@@ -4,7 +4,7 @@ modify fun s => s - v
 get
 
 def g : IO Nat :=
-f 5 $.run' 20
+f 5 |>.run' 20
 
 #eval (f 5).run' 20
 
@@ -50,7 +50,7 @@ IO.println $ "state1 " ++ toString a1
 IO.println $ "state1 " ++ toString a2
 pure (a0 + a1 + a2)
 
-#eval f4.run' ⟨10⟩ $.run' ⟨20⟩ $.run' ⟨30⟩
+#eval f4.run' ⟨10⟩ |>.run' ⟨20⟩ |>.run' ⟨30⟩
 
 abbrev S (ω : Type) := StateRefT Nat $ StateRefT String $ ST ω
 
@@ -60,6 +60,6 @@ modify fun n => n + s.length
 pure ()
 
 def f5Pure (n : Nat) (s : String) :=
-runST fun _ => f5.run n $.run s
+runST fun _ => f5.run n |>.run s
 
 #eval f5Pure 10 "hello world"