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

Fix typo in FC.idr.

Browse Source 
Change "beeen" to "been".
This commit is contained in:
Dong Tsing-hsuen 2021-02-15 21:04:54 +08:00 committed by G. Allais
parent 8c7a08f282
commit 447110c686
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/Core/FC.idr
View File

@ -21,7 +21,7 @@ FileName : Type
FileName = String
||| A file context is a filename together with starting and ending positions.
||| It's often carried by AST nodes that might have beeen created from a source
||| It's often carried by AST nodes that might have been created from a source
||| file or by the compiler. That makes it useful to have the notion of
||| `EmptyFC` as part of the type.
public export