Improve documentation for WordMap

[langston-barrett]

The constructor of WordMap has two fields, and at first glance, it's not at all clear how, together, they implement the functionality described in the Haddock:

what4/what4/src/What4/WordMap.hs

Lines 32 to 38 in 85e68eb

	-- | A @WordMap@ represents a finite partial map from bitvectors of width @w@
	-- to elements of type @tp@.
	data WordMap sym w tp =
	SimpleWordMap !(SymExpr sym
	(BaseArrayType (EmptyCtx ::> BaseBVType w) BaseBoolType))
	!(SymExpr sym
	(BaseArrayType (EmptyCtx ::> BaseBVType w) tp))

After a bit of reading, it appears that the first field consists of a map from bitvectors to predicates which indicates when a given index is defined, and the second is a mapping from bitvectors to values (which, presumably, are only "valid" when the corresponding Pred is true?). This should be described in the Haddock, along with any potential invariants (e.g., is it the case that lookupWordMap should succeed after insertWordMap? Likely, such invariants couldn't be enforced at the moment, as the constructor is exported).