idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-19 17:21:59 +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:49:27 +09:00
parent 0dfecf87df
commit c4eaacc493
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

@ -493,7 +493,7 @@ typebindDoc = """
use it on the right-hand-side.
A typical example of a typebind operator is `(**)` the type constructor
for dependent pairs. It is used like this: `(x : Nat ** Vect x String)`
for dependent pairs. It is used like this: `(x : Nat) ** Vect x String`
If you declare a new operator to be typebind you can use it the same
way.