idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-09-21 02:07:25 +03:00
Code Issues Projects Releases Wiki Activity

Remove forgotten .field from docs.

Browse Source
This commit is contained in:
Matus Tejiscak 2020-06-20 23:52:42 +02:00 committed by G. Allais
parent b46064f688
commit 3b6d7a22e3
1 changed files with 2 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
docs/source/tutorial/typesfuns.rst
View File

@ -988,8 +988,8 @@ type. The field names can be used to access the field values:
"Fred" : String
*Record> fred.age
30 : Int
*Record> :t (.firstName)
Main.Person.(.firstName) : Person -> String
*Record> :t firstName
firstName : Person -> String
We can use prefix field projections, like in Haskell:
@ -999,8 +999,6 @@ We can use prefix field projections, like in Haskell:
"Fred" : String
*Record> age fred
30 : Int
*Record> :t firstName
firstName : Person -> String
We can also use the field names to update a record (or, more
precisely, produce a copy of the record with the given fields