idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-28 02:23:44 +03:00
Code Issues Projects Releases Wiki Activity

Typo

Browse Source
This commit is contained in:
russoul 2020-09-01 16:18:13 +03:00
parent a6d767f8fa
commit 394b433c59
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
tests/idris2/record006/Fld.idr
View File

@ -7,7 +7,7 @@ import Data.Maybe
-- What would be a reason to have named constructors anyway, if we were to instantiate records by their
-- type constructors ?
-- Also it turned out that specifing type constructors instead of data constructors
-- Also it turned out that specifying type constructors instead of data constructors
-- does not simplify or provide any other benifit in internal implementation.