This library provides combinators and typeclasses for working and manipulating
type-level predicates in Haskell, which are represented as matchable type-level
functions k ~> Type from the singletons library. See Data.Type.Predicate
for a good starting point, and the documentation for Predicate on how to
define predicates.
Added tripleNegation and negateTwice to Data.Type.Predicate.Logic,
for more constructivist principles.
Renamed excludedMiddle to complementation.
Add TyPP, SearchableTC, searchTC, SelectableTC, selectTC to
Data.Type.Predicate.Param, to mirror TyPred and the
DecidableTC/ProvableTC interface from Data.Type.Predicate
New :.: for universe composition, with Elem and Universe instances,
and associated functions for working with them alongside Any, All.
Many of the Elem instances and indices in Data.Type.Universe have had
their name changed to be more consistent with their role as indices.
IsJust is now IJust, IsRight is IRight, Snd is ISnd.
Convenience predicates for alternate universes, such as IsJust, IsLeft,
IsNothing, etc.
NotAll quantifier added alongside None.
Many new implications added to Data.Type.Predicate.Quantification,
converting not-any and all-not, etc.
NotFound p added as a convenience predicate synonym for Not (Found p).
Some implications showing the equivalence between Found (InP f) and
NotNull f added to Data.Type.Predicate.Param.
Many new deduction rules added to Data.Type.Predicate.Auto. Please see
module documentation for a detailed list of new rules and classes in this
version.
Convenient combinators for dealing with Refuted and Decision added to
Data.Type.Predicate: elimDisproof and mapRefuted.
