1
1
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-25 12:42:02 +03:00
Idris2/tests/idris2/warning003/expected

12 lines
337 B
Plaintext

1/1: Building Main (Main.idr)
Warning: DEPRECATED: old record update syntax. Use "{ f := v } p" instead of "record { f = v } p"
Main:11:14--11:37
07 | testRec : TestRecord
08 | testRec = MkTestRecord 0
09 |
10 | updatedRec : TestRecord
11 | updatedRec = record { recField = 1 } testRec
^^^^^^^^^^^^^^^^^^^^^^^