BSD-3-Clause licensed by Justin Le
Maintained by

Module documentation for

This version can be pinned in stack with:list-witnesses-,1670


list-witnesses on Hackage

Collection of assorted inductive witnesses and functions for working with type-level lists.

  • Data.Type.List.Edit contains single-item edits of lists, including insertion, deletion, and substitution.
  • Data.Type.List.Sublist contains witnesses for prefixes, suffixes, and two-way splits of type-level lists.




August 25, 2019

  • Fixed overlapping instance issues resulting from ambiguities in Auto instances for Insert, Delete, Substitute, Suffix, Interleave, and Subset.


August 23, 2019

  • Quick renaming of subsetToInterlaveLeft and subsetToInterleaveRight to match naming conventions.


August 23, 2019

  • Add Subset and associated methods
  • interleaveShapes, swapInterleave, appendShape, prefixShape


August 12, 2019

  • Add predicates (IsInsert, IsPrefix, etc.) and Auto and Decidable instances for most of the data types, for auto-generation and searches.
  • Add some functions for creating Appends and witnesses of concatenation type families from Appends.
  • interleavedIxes, for more manipulation of Interleave


August 3, 2019

  • Add microlens as a dependency, and use actual type synonyms for lenses. Also got rid of re-implementations of over and view.


March 7, 2019

  • Add Interleave to Data.Type.List.Sublist.


March 6, 2019

  • Initial release
comments powered byDisqus