From 1230a76c1ebe08c21e1b13acc3b2c604ab5d38d3 Mon Sep 17 00:00:00 2001
From: Andre Videla <andre.videla@gmail.com>
Date: Fri, 15 Dec 2023 18:24:33 +0000
Subject: [PATCH] update comment documentation strings

---
 src/Core/TT.idr       | 14 +++++++-------
 src/Idris/Desugar.idr |  6 +++---
 src/Idris/Parser.idr  | 10 +++++-----
 3 files changed, 15 insertions(+), 15 deletions(-)

diff --git a/src/Core/TT.idr b/src/Core/TT.idr
index e20887c008..5727cf0b34 100644
--- a/src/Core/TT.idr
+++ b/src/Core/TT.idr
@@ -173,25 +173,25 @@ Eq FixityInfo where
 -- Left-hand-side information for operators, carries autobind information
 -- an operator can either be
 -- - not autobind, a regular operator
--- - binding types, such that (nm : ty ** fn nm) desugars into (ty ** \(nm : ty) => fn nm)
+-- - binding types, such that `(nm : ty) =@ fn nm` desugars into `(=@) ty (\(nm : ty) => fn nm)`
 -- - binding expressing with an inferred type such that
---   (nm := exp ** fn nm) desugars into (exp ** \(nm : ?) => fn nm)
+--   `(nm := exp) =@ fn nm` desugars into `(=@) exp (\(nm : ?) => fn nm)`
 -- - binding both types and expression such that
---   (nm : ty := exp ** fn nm) desugars into (exp ** \(nm : ty) => fn nm)
+--   `(nm : ty := exp) =@ fn nm` desugars into `(=@) exp (\(nm : ty) => fn nm)`
 public export
 data OperatorLHSInfo : tm -> Type where
   -- Traditional operator wihtout binding, carries the lhs
   NoBinder : (lhs : tm) -> OperatorLHSInfo tm
-  -- (nm : ty) ** fn x
+  -- (nm : ty) =@ fn x
   BindType : (name : WithBounds Name) -> (ty : tm) -> OperatorLHSInfo tm
-  -- (nm := exp) ** fn nm
+  -- (nm := exp) =@ fn nm
   BindExpr : (name : WithBounds Name) -> (expr : tm) -> OperatorLHSInfo tm
-  -- (nm : ty := exp) ** fn nm
+  -- (nm : ty := exp) =@ fn nm
   BindExplicitType : (name : WithBounds Name) ->  (type, expr : tm) -> OperatorLHSInfo tm
 
 export
 Show (OperatorLHSInfo tm) where
-  show (NoBinder lhs)                 = "regular"
+  show (NoBinder lhs)                    = "regular"
   show (BindType name ty)                = "type-binding (typebind)"
   show (BindExpr name expr)              = "automatically-binding (autobind)"
   show (BindExplicitType name type expr) = "automatically-binding (autobind)"
diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr
index b91ba7c842..c5efa8eab6 100644
--- a/src/Idris/Desugar.idr
+++ b/src/Idris/Desugar.idr
@@ -780,19 +780,19 @@ mutual
       = do l' <- desugarTree side ps l
            r' <- desugarTree side ps r
            pure (IApp loc (IApp loc (IVar opFC op) l') r')
-  -- (x : ty ** f x) ==>> (**) exp (\x : ty => f x)
+  -- (x : ty) =@ f x ==>> (=@) exp (\x : ty => f x)
   desugarTree side ps (Infix loc opFC (op, Just (BindType name lhs)) _ r)
       = do desugaredLHS <- desugarB side ps lhs
            desugaredRHS <- desugarTree side ps r
            pure $ IApp loc (IApp loc (IVar opFC op) desugaredLHS)
                            (ILam loc top Explicit (Just name.val) desugaredLHS desugaredRHS)
-  -- (x := exp ** f x) ==>> (**) exp (\x : ? => f x)
+  -- (x := exp) =@ f x ==>> (=@) exp (\x : ? => f x)
   desugarTree side ps (Infix loc opFC (op, Just (BindExpr name lhs)) _ r)
       = do desugaredLHS <- desugarB side ps lhs
            desugaredRHS <- desugarTree side ps r
            pure $ IApp loc (IApp loc (IVar opFC op) desugaredLHS)
                            (ILam loc top Explicit (Just name.val) (Implicit opFC False) desugaredRHS)
-  -- (x : ty := exp ** f x) ==>> (**) exp (\x : ty => f x)
+  -- (x : ty := exp) =@ f x ==>> (=@) exp (\x : ty => f x)
   desugarTree side ps (Infix loc opFC (op, Just (BindExplicitType name ty expr)) _ r)
       = do desugaredLHS <- desugarB side ps expr
            desugaredType <- desugarB side ps ty
diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr
index 9abeb7c692..14ab15a5d6 100644
--- a/src/Idris/Parser.idr
+++ b/src/Idris/Parser.idr
@@ -1882,16 +1882,16 @@ definition fname indents
     = do nd <- bounds (clause 0 Nothing fname indents)
          pure (PDef (boundToFC fname nd) [nd.val])
 
-operatorBindingKeyword : EmptyRule BindingModifier
-operatorBindingKeyword
-  =   (keyword "autobind" >> pure Autobind)
-  <|> (keyword "typebind" >> pure Typebind)
+operatorBindingKeyword : OriginDesc -> EmptyRule BindingModifier
+operatorBindingKeyword fname
+  =   (decoratedKeyword fname "autobind" >> pure Autobind)
+  <|> (decoratedKeyword fname "typebind" >> pure Typebind)
   <|> pure NotBinding
 
 fixDecl : OriginDesc -> IndentInfo -> Rule (List PDecl)
 fixDecl fname indents
     = do vis <- exportVisibility fname
-         binding <- operatorBindingKeyword
+         binding <- operatorBindingKeyword fname
          b <- bounds (do fixity <- decorate fname Keyword $ fix
                          commit
                          prec <- decorate fname Keyword $ intLit