AltList.idr

module Data.AltList

%access public export
%default total

data AltList : (a : Type) -> (b : Type) -> Type where
  Nil : AltList a b
  ConsB : b -> AltList a b -> AltList a b
  ConsAB : a -> b -> AltList a b -> AltList a b

data IsConsB : AltList a b -> Type where
  ItIsConsB : IsConsB (ConsB x xs)

namespace ConsB
  (::) : b -> AltList a b -> AltList a b
  (::) = ConsB

namespace ConsA
  (::) : a -> (xs : AltList a b) -> {auto ok : IsConsB xs} -> AltList a b
  (::) x (ConsB y xs) = ConsAB x y xs

stringIntList : AltList String Int
stringIntList = ["hello", 1, "world", 2]

This allows any number of bs in sequence, rather than requiring them to alternate.