Idris2/tests/base/data_list001/expected

mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-20 18:21:47 +03:00
1/1: Building List (List.idr)
Main> [[], [4], [3], [4, 5], [3, 5], [3, 4]]
[[6], [6, 4], [3, 6], [6, 4, 5], [3, 6, 5], [3, 4, 6]]
Main> Bye for now!
add deleteAt for List (#2317) 2022-02-11 12:28:36 +03:00			`1/1: Building List (List.idr)`
			`Main> [[], [4], [3], [4, 5], [3, 5], [3, 4]]`
add `replaceAt` for `List` (#2335) 2022-03-04 02:40:18 +03:00			`[[6], [6, 4], [3, 6], [6, 4, 5], [3, 6, 5], [3, 4, 6]]`
add deleteAt for List (#2317) 2022-02-11 12:28:36 +03:00			`Main> Bye for now!`