Map package:leancheck

Lists of pairs representing maps. The Listable tiers enumeration will not have repeated maps.

> take 6 (list :: [Map Nat Nat])
[Map [],Map [(0,0)],Map [(0,1)],Map [(1,0)],Map [(0,2)],Map [(1,1)]]

Given a constructor that takes a map of elements (encoded as a list), lists tiers of applications of this constructor So long as the underlying Listable enumerations have no repetitions, this will generate no repetitions. This allows defining an efficient implementation of tiers that does not repeat maps given by:

tiers  =  mapCons fromList

map over tiers

mapT f [[x], [y,z], [w,...], ...]  =  [[f x], [f y, f z], [f w, ...], ...]

mapT f [xs, ys, zs, ...]  =  [map f xs, map f ys, map f zs]

Like mapMaybe but for tiers.

Takes as arguments tiers of source and target values; returns tiers of maps from the source to the target encoded as lists without repetition.

concatMap over tiers

concatMapT f [ [x0, y0, z0]
, [x1, y1, z1]
, [x2, y2, z2]
, ...
]
=  f x0 \/ f y0 \/ f z0 \/ ...
\/ delay (f x1 \/ f y1 \/ f z1 \/ ...
\/ delay (f x2 \/ f y2 \/ f z2 \/ ...
\/ (delay ...)))

(cf. concatT)