diff --git a/src/Idris/Doc/Keywords.idr b/src/Idris/Doc/Keywords.idr index b79d64485..0f1d4a408 100644 --- a/src/Idris/Doc/Keywords.idr +++ b/src/Idris/Doc/Keywords.idr @@ -469,18 +469,19 @@ autobindDoc = """ `autobind` differs from `typebind` in the syntax it allows and the way it desugars. Delcaring an operator as `autobind infixr 0 =|>` allows - you to use it with the syntax `(x := e =|> f x)` or `(x : t := e =|> f x)` + you to use it with the syntax `(x := e) =|> f x`, `(x : t := e) =|> f x`. + You will need to use `autobind` instead of `typebind` whenever the type of the lambda of the function called by the operator has a type - that is not equal to the argument given on the left side of the operator + that is not equal to the argument given on the left side of the operator. `autobind` only applies to `infixr` operators and cannot be used as operator sections. `autobind` operators are desugared as a lambda: - `(x := expr =|> fn x)` -> `(expr =@ (\x : ? =|> fn x))` - `(x : ty := expr =|> fn x)` -> `(expr =@ (\x : ty =|> fn x))` + `(x := expr) =|> fn x` -> `(expr =@ (\x : ? =|> fn x))` + `(x : ty := expr) =|> fn x` -> `(expr =@ (\x : ty =|> fn x))` """ typebindDoc : Doc IdrisDocAnn typebindDoc = """ @@ -498,13 +499,13 @@ typebindDoc = """ way. Start by defining `typebind infixr 1 =@`, and then you can use it - like so: `(n : Nat =@ f n)` or `(n : Nat) =@ f n` + like so: `(n : Nat) =@ f n` `typebind` only applies to `infixr` operators and cannot be used as operator sections. `typebind` operators are desugared as a lambda: - `(x : ty =@ fn x)` -> `(ty =@ (\x : ty =@ fn x))` + `(x : ty) =@ fn x` -> `(ty =@ (\x : ty =@ fn x))` """ rewriteeq : Doc IdrisDocAnn