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

Update src/Idris/Doc/Keywords.idr

Browse Source
This commit is contained in:
André Videla 2024-01-23 19:46:07 +09:00
parent 2859fcee08
commit b48a2d11f0
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -498,7 +498,7 @@ typebindDoc = """
If you declare a new operator to be typebind you can use it the same If you declare a new operator to be typebind you can use it the same
way. way.
Start by defining `typebind infixr 1 =@`, and then you can use it Start by defining `typebind infixr 0 =@`, and then you can use it
like so: `(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