list-witnesses

Witnesses for working with type-level lists

BSD-3-Clause licensed by Justin Le

Maintained by [email protected]

This version can be pinned in stack with:list-witnesses-0.1.2.0@sha256:5f18b7fcbe7915c3e75a19184926ab3344970cfecdc4d7a53d4d1d15865f99fc,1670

Depends on 7 packages(full list with versions):

[list-witnesses][docs]

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 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

March 6, 2019