idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-24 12:14:26 +03:00
Code Issues Projects Releases Wiki Activity

fix repl documentation

Browse Source
This commit is contained in:
André Videla 2023-11-01 23:12:27 +00:00
parent 07c42c22a5
commit d49f008cb5
1 changed files with 7 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
src/Idris/Doc/Keywords.idr
View File

@ -469,18 +469,19 @@ autobindDoc = """
`autobind` differs from `typebind` in the syntax it allows and the way `autobind` differs from `typebind` in the syntax it allows and the way
it desugars. Delcaring an operator as `autobind infixr 0 =|>` allows 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 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 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 `autobind` only applies to `infixr` operators and cannot be used as
operator sections. operator sections.
`autobind` operators are desugared as a lambda: `autobind` operators are desugared as a lambda:
`(x := expr =|> fn x)` -> `(expr =@ (\x : ? =|> fn x))` `(x := expr) =|> fn x` -> `(expr =@ (\x : ? =|> fn x))`
`(x : ty := expr =|> fn x)` -> `(expr =@ (\x : ty =|> fn x))` `(x : ty := expr) =|> fn x` -> `(expr =@ (\x : ty =|> fn x))`
""" """
typebindDoc : Doc IdrisDocAnn typebindDoc : Doc IdrisDocAnn
typebindDoc = """ typebindDoc = """
@ -498,13 +499,13 @@ typebindDoc = """
way. way.
Start by defining `typebind infixr 1 =@`, and then you can use it 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 `typebind` only applies to `infixr` operators and cannot be used as
operator sections. operator sections.
`typebind` operators are desugared as a lambda: `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 rewriteeq : Doc IdrisDocAnn