Agda.Utils.List2

O(length first list).

O(length first list).

Concatenate at least 2 lists of length at least 1.

O(1).

Unsafe! O(1).

Any List1 is either a singleton or a List2. O(1).

Safe. O(1).

Safe. O(1).

Safe. O(1).

Safe. O(n).

O(n).

Safe. O(1).

Safe. O(1).

Inverse of fromList1Either. O(1).

Lists of length ≥2.

The toList function extracts a list of Item l from the structure l. It should satisfy fromList . toList = id.