mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-20 01:41:44 +03:00
Update src/Idris/Doc/Keywords.idr
This commit is contained in:
parent
93de3e0e07
commit
48618490d0
@ -480,8 +480,8 @@ autobindDoc = """
|
|||||||
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 = """
|
||||||
|
Loading…
Reference in New Issue
Block a user