Changelog
Version 0.3.1.1
February 27, 2024
https://github.com/mstksg/functor-products/releases/tag/v0.3.1.1
- Remove upper bounds and deprecated pragmas
Version 0.3.1.0
July 4, 2023
https://github.com/mstksg/functor-products/releases/tag/v0.3.1.0
- Now requires singletons-3.0 and above, and GHC 9.2 and above
Version 0.3.0.0
Feburary 2, 2020
https://github.com/mstksg/decidable/releases/tag/v0.3.0.0
- Update to work with singletons-2.6, the type family update
- Change Evidentto now be a defunctionalization symbol forSing, instead
of a type synonym withTyPred, to match with singletons-2.6.  Most code
in practice should be the same.
- Fix instances for FProds: now can prove and decide anyFProd f (Wit p),
and can prove and decide and auto anyFProd f WrappedSing.
Version 0.2.1.0
August 24, 2019
https://github.com/mstksg/decidable/releases/tag/v0.2.1.0
- Add autoTCfor convenient usage ofautowith type constructors.
Version 0.2.0.0
August 12, 2019
https://github.com/mstksg/decidable/releases/tag/v0.2.0.0
- Full restructuring of the Universe system, pulling it all out into a new
package, functor-products.
Version 0.1.5.0
March 6, 2018
https://github.com/mstksg/decidable/releases/tag/v0.1.5.0
- Add allToAnyto Data.Type.Predicate.Quantification.
- Add PPMapV,EqBy, andIsTCto Data.Type.Predicate.Param.
- Kind-indexed singletons for indices in Data.Type.Universe.
Version 0.1.4.0
October 29, 2018
https://github.com/mstksg/decidable/releases/tag/v0.1.4.0
- Added tripleNegationandnegateTwiceto Data.Type.Predicate.Logic,
for more constructivist principles.
- Renamed excludedMiddletocomplementation.
- Add TyPP,SearchableTC,searchTC,SelectableTC,selectTCto
Data.Type.Predicate.Param, to mirrorTyPredand theDecidableTC/ProvableTCinterface from Data.Type.Predicate
Version 0.1.3.1
October 26, 2018
https://github.com/mstksg/decidable/releases/tag/v0.1.3.1
- BUGFIX Remove overlapping Autoinstances forIsNothingandIsLeft.
Version 0.1.3.0
October 24, 2018
https://github.com/mstksg/decidable/releases/tag/v0.1.3.0
- Added a type and Universefor universe disjunction or summing,:+:,
with appropriateElemandAutoinstances.
- Added Universeinstances (and appropriateElemandAutoinstances)
forProxy(the null universe) andIdentity.
- Autoinstances for- IsNothingand- IsLeft.
Version 0.1.2.0
October 14, 2018
https://github.com/mstksg/decidable/releases/tag/v0.1.2.0
- New :.:for universe composition, withElemandUniverseinstances,
and associated functions for working with them alongsideAny,All.
- Many of the Eleminstances and indices in Data.Type.Universe have had
their name changed to be more consistent with their role as indices.IsJustis nowIJust,IsRightisIRight,SndisISnd.
- Convenience predicates for alternate universes, such as IsJust,IsLeft,IsNothing, etc.
- NotAllquantifier added alongside- None.
- Many new implications added to Data.Type.Predicate.Quantification,
converting not-any and all-not, etc.
- NotFound padded as a convenience predicate synonym for- Not (Found p).
- Some implications showing the equivalence between Found (InP f)andNotNull fadded 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 RefutedandDecisionadded to
Data.Type.Predicate:elimDisproofandmapRefuted.
Version 0.1.1.0
October 12, 2018
https://github.com/mstksg/decidable/releases/tag/v0.1.1.0
- flipDecision,- forgetDisproof,- forgetProof,- isProved, and- isDisprovedadded to Data.Type.Predicate module.
- ProvableTC,- DeccidableTC,- proveTC, and- decideTChelper functions
and constraints
- Data.Type.Predicate.Auto module, for generating witnesses at
compile-time.
- Instances for injection and projection out of &&&and|||, with some
tricks to prevent overlapping instance issues.
Version 0.1.0.0
October 10, 2018
https://github.com/mstksg/decidable/releases/tag/v0.1.0.0