mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-30 07:02:24 +03:00
81 lines
12 KiB
Plaintext
81 lines
12 KiB
Plaintext
|
000018(:protocol-version 2 0)
|
||
|
|
000042(:write-string "1/1: Building RecordUpdate (RecordUpdate.idr)" 1)
|
||
|
|
000077(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 1 1) (:end 1 6)) ((:decor :keyword)))))) 1)
|
||
|
|
000077(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 3 1) (:end 3 6)) ((:decor :keyword)))))) 1)
|
||
|
|
000075(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 3 8) (:end 3 17)) ((:decor :type)))))) 1)
|
||
|
|
000079(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 3 19) (:end 3 23)) ((:decor :keyword)))))) 1)
|
||
|
|
000078(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 4 3) (:end 4 6)) ((:decor :function)))))) 1)
|
||
|
|
000077(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 4 8) (:end 4 8)) ((:decor :keyword)))))) 1)
|
||
|
|
000076(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 4 10) (:end 4 15)) ((:decor :type)))))) 1)
|
||
|
|
000078(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 5 3) (:end 5 6)) ((:decor :function)))))) 1)
|
||
|
|
000077(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 5 8) (:end 5 8)) ((:decor :keyword)))))) 1)
|
||
|
|
0000dc(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 5 10) (:end 5 12)) ((:name "Nat") (:namespace "Prelude.Types") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||
|
|
0000dc(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 5 10) (:end 5 12)) ((:name "Nat") (:namespace "Prelude.Types") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||
|
|
0000dc(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 5 10) (:end 5 12)) ((:name "Nat") (:namespace "Prelude.Types") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||
|
|
000078(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 7 1) (:end 7 7)) ((:decor :function)))))) 1)
|
||
|
|
000077(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 7 9) (:end 7 9)) ((:decor :keyword)))))) 1)
|
||
|
|
0000e2(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 7 11) (:end 7 20)) ((:name "Attributes") (:namespace "RecordUpdate") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||
|
|
000079(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 7 22) (:end 7 23)) ((:decor :keyword)))))) 1)
|
||
|
|
0000e2(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 7 25) (:end 7 34)) ((:name "Attributes") (:namespace "RecordUpdate") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||
|
|
0000e1(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 8 1) (:end 8 7)) ((:name "bigMono") (:namespace "RecordUpdate") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||
|
|
000077(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 8 9) (:end 8 9)) ((:decor :keyword)))))) 1)
|
||
|
|
000079(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 8 11) (:end 8 16)) ((:decor :keyword)))))) 1)
|
||
|
|
000079(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 8 18) (:end 8 18)) ((:decor :keyword)))))) 1)
|
||
|
|
00007a(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 8 20) (:end 8 23)) ((:decor :function)))))) 1)
|
||
|
|
000079(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 8 25) (:end 8 26)) ((:decor :keyword)))))) 1)
|
||
|
|
000079(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 8 28) (:end 8 28)) ((:decor :keyword)))))) 1)
|
||
|
|
0000e6(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 8 29) (:end 8 30)) ((:name "++") (:namespace "Prelude.Types.String") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||
|
|
000076(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 8 32) (:end 8 37)) ((:decor :data)))))) 1)
|
||
|
|
000079(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 8 38) (:end 8 38)) ((:decor :keyword)))))) 1)
|
||
|
|
000079(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 9 18) (:end 9 18)) ((:decor :keyword)))))) 1)
|
||
|
|
00007a(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 9 20) (:end 9 23)) ((:decor :function)))))) 1)
|
||
|
|
000079(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 9 25) (:end 9 25)) ((:decor :keyword)))))) 1)
|
||
|
|
000076(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 9 27) (:end 9 28)) ((:decor :data)))))) 1)
|
||
|
|
00007b(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 10 18) (:end 10 18)) ((:decor :keyword)))))) 1)
|
||
|
|
00007a(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 12 1) (:end 12 9)) ((:decor :function)))))) 1)
|
||
|
|
00007b(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 12 11) (:end 12 11)) ((:decor :keyword)))))) 1)
|
||
|
|
0000e4(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 12 13) (:end 12 22)) ((:name "Attributes") (:namespace "RecordUpdate") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||
|
|
00007b(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 12 24) (:end 12 25)) ((:decor :keyword)))))) 1)
|
||
|
|
0000e4(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 12 27) (:end 12 36)) ((:name "Attributes") (:namespace "RecordUpdate") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||
|
|
0000e5(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 13 1) (:end 13 9)) ((:name "smallMono") (:namespace "RecordUpdate") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||
|
|
00007b(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 13 11) (:end 13 11)) ((:decor :keyword)))))) 1)
|
||
|
|
00007b(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 13 13) (:end 13 13)) ((:decor :keyword)))))) 1)
|
||
|
|
00007c(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 13 15) (:end 13 18)) ((:decor :function)))))) 1)
|
||
|
|
00007b(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 13 20) (:end 13 21)) ((:decor :keyword)))))) 1)
|
||
|
|
000078(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 13 23) (:end 13 23)) ((:decor :data)))))) 1)
|
||
|
|
00007b(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 13 25) (:end 13 25)) ((:decor :keyword)))))) 1)
|
||
|
|
0000e1(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 13 27) (:end 13 27)) ((:name ".") (:namespace "Prelude.Basics") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||
|
|
0000e5(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 13 29) (:end 13 35)) ((:name "bigMono") (:namespace "RecordUpdate") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||
|
|
000079(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 16 1) (:end 16 6)) ((:decor :keyword)))))) 1)
|
||
|
|
000077(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 16 8) (:end 16 11)) ((:decor :type)))))) 1)
|
||
|
|
00007b(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 16 13) (:end 16 17)) ((:decor :keyword)))))) 1)
|
||
|
|
00007b(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 17 3) (:end 17 12)) ((:decor :function)))))) 1)
|
||
|
|
00007b(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 17 14) (:end 17 14)) ((:decor :keyword)))))) 1)
|
||
|
|
0000e4(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 17 16) (:end 17 25)) ((:name "Attributes") (:namespace "RecordUpdate") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||
|
|
0000e4(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 17 16) (:end 17 25)) ((:name "Attributes") (:namespace "RecordUpdate") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||
|
|
0000e4(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 17 16) (:end 17 25)) ((:name "Attributes") (:namespace "RecordUpdate") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||
|
|
00007a(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 18 3) (:end 18 9)) ((:decor :function)))))) 1)
|
||
|
|
00007b(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 18 11) (:end 18 11)) ((:decor :keyword)))))) 1)
|
||
|
|
000078(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 18 13) (:end 18 18)) ((:decor :type)))))) 1)
|
||
|
|
00007b(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 20 1) (:end 20 10)) ((:decor :function)))))) 1)
|
||
|
|
00007b(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 20 12) (:end 20 12)) ((:decor :keyword)))))) 1)
|
||
|
|
0000de(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 20 14) (:end 20 17)) ((:name "Text") (:namespace "RecordUpdate") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||
|
|
00007b(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 20 19) (:end 20 20)) ((:decor :keyword)))))) 1)
|
||
|
|
0000de(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 20 22) (:end 20 25)) ((:name "Text") (:namespace "RecordUpdate") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||
|
|
0000e7(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 21 1) (:end 21 10)) ((:name "setArial10") (:namespace "RecordUpdate") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||
|
|
00007b(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 21 12) (:end 21 12)) ((:decor :keyword)))))) 1)
|
||
|
|
00007b(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 21 14) (:end 21 14)) ((:decor :keyword)))))) 1)
|
||
|
|
00007c(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 21 16) (:end 21 25)) ((:decor :function)))))) 1)
|
||
|
|
00007b(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 21 26) (:end 21 27)) ((:decor :keyword)))))) 1)
|
||
|
|
00007c(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 21 28) (:end 21 31)) ((:decor :function)))))) 1)
|
||
|
|
00007b(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 21 33) (:end 21 34)) ((:decor :keyword)))))) 1)
|
||
|
|
000078(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 21 36) (:end 21 42)) ((:decor :data)))))) 1)
|
||
|
|
00007b(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 22 14) (:end 22 14)) ((:decor :keyword)))))) 1)
|
||
|
|
00007c(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 22 16) (:end 22 25)) ((:decor :function)))))) 1)
|
||
|
|
00007c(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 22 26) (:end 22 30)) ((:decor :function)))))) 1)
|
||
|
|
00007b(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 22 32) (:end 22 33)) ((:decor :keyword)))))) 1)
|
||
|
|
000078(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 22 35) (:end 22 36)) ((:decor :data)))))) 1)
|
||
|
|
00007b(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 23 14) (:end 23 14)) ((:decor :keyword)))))) 1)
|
||
|
|
000015(:return (:ok ()) 1)
|
||
|
|
Alas the file is done, aborting
|