!^Q      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~(c) Justin Le 2018BSD3 justin@jle.im experimental non-portableNone&'+,-7;<=>?AFQSTV]dit# decidable p is the predicate that p is not true. decidable Implicatons p  q can be lifted "through" a  into an f p  f q. decidable Implicatons p  q can be lifted "through" a  into an f p  f q. decidableIf  T :: k ->  is a type constructor, then  T is a constraint that T8 is "decidable", in that you have a canonical function: proveTC :: Sing a -> T a Is essentially  , except with type constructors k -> 6 instead of matchable type-level functions (that are k ~> ).  decidableIf  T :: k ->  is a type constructor, then   T is a constraint that T8 is "decidable", in that you have a canonical function: decideTC :: Sing a ->  (T a) Is essentially  , except with type constructors k -> 5 instead of matchable type-level functions (that are k ~> ).  decidable  p is a constraint that p can be disproven.  decidableAA typeclass for provable predicates (constructivist tautologies).,A predicate is provable if, given any input a, you can generate a proof of p @@ a<. Essentially, it means that a predicate is "always true".SThis typeclass associates a canonical proof function for every provable predicate.It confers two main advatnages: JThe proof function for every predicate is available via the same name We can write   instances for polymorphic predicate transformers (predicates parameterized on other predicates) easily, by refering to  ) instances of the transformed predicates.  decidable-The canonical proving function for predicate p. Note that   is ambiguously typed, so you always\ need to call by specifying the predicate you want to prove using TypeApplications syntax:   @MyPredicate  decidable%A typeclass for decidable predicates.-A predicate is decidable if, given any input a$, you can either prove or disprove p @@ a. A  (p @@ a)# is a data type that has a branch p @@ a and  (p @@ a).WThis typeclass associates a canonical decision function for every decidable predicate.It confers two main advatnages: MThe decision function for every predicate is available via the same name We can write   instances for polymorphic predicate transformers (predicates parameterized on other predicates) easily, by refering to  ) instances of the transformed predicates. decidable.The canonical decision function for predicate p. Note that  is ambiguously typed, so you always\ need to call by specifying the predicate you want to prove using TypeApplications syntax:  @MyPredicate  decidableThis is implication !, but only in a specific context h. decidable We say that p implies q (p  q ) if, given p  a, we can always prove q @@ a. decidable!A proving function for predicate p. See   for more information. decidableLike !, but only in a specific context h. decidableLike implication , but knowing p @@ a" can only let us decidably prove q  a is true or false. decidable"A decision function for predicate p. See   for more information. decidableA  p a is a value of type p @@ a- --- that is, it is a proof or witness that p is satisfied for a.It essentially turns a k ~>  ("matchable"  k) /back into/ a k ->  predicate. decidable%Pre-compose a function to a predicate  :: (k ~> j) ->  j -> Predicate k  decidableConvert a tradtional k ~>  predicate into a .  :: (k ~> Bool) -> Predicate k  decidable a+ is a predicate that the input is equal to a. decidableThe always-false predicateCould also be defined as  Void&, but this defintion gives us a free   instance. decidableThe always-true predicate.  ::  k  decidableConvert a normal '->' type constructor into a .  :: (k -> ) ->  k  decidable>A type-level predicate in Haskell. We say that the predicate P ::  k is true/satisfied by input x :: k" if there exists a value of type P @@ xD, and that it false/disproved if such a value cannot exist. (Where  is S, the singleton library's type-level function application for mathcable functions)See   and  H for more information on how to use, prove and decide these predicates. The kind k ~>  is the kind of "matchable" type-level functions in Haskell. They are type-level functions that are encoded as dummy type constructors ("defunctionalization symbols") that can be decidedly "matched" on for things like typeclass instances.1There are two ways to define your own predicates: XUsing the predicate combinators and predicate transformers in this library and the  singletonsv library, which let you construct pre-made predicates and sometimes create predicates from other predicates.AManually creating a data type that acts as a matchable predicate.\For an example of the latter, we can create the "not p" predicate, which takes a predicate p5 as input and returns the negation of the predicate: {-- First, create the data type with the kind signature you want data Not :: Predicate k -> Predicate k -- Then, write the N instance, to specify the type of the -- witnesses of that predicate instance  (Not p) a = (p  a) -> Void See the source of Data.Type.Predicate and Data.Type.Predicate.Logic` for simple examples of hand-made predicates. For example, we have the always-true predicate : >data Evident :: Predicate k instance Apply Evident a = Sing a #And the "and" predicate combinator: Xdata (&&&) :: Predicate k -> Predicate k -> Predicate k instance Apply (p &&& q) a = (p  a, q  a) [Typically it is recommended to create predicates from the supplied predicate combinators (d can be used for any type constructor to turn it into a predicate, for instance) whenever possible. decidable%The deciding/disproving function for   p.Must be called by applying the  to disprove:  @p  decidable$The canonical deciding function for   t.! decidable#The canonical proving function for   t." decidableCompose two implications.# decidableDecide Not p based on decisions of p.$ decidable2Flip the contents of a decision. Turn a proof of a into a disproof of not-a.>Note that this is not reversible in general in Haskell. See doubleNegation for a situation where it is.% decidableMap over the value inside a .& decidable Converts a  to a $. Drop the witness of disproof of a , returning  if  (with the proof) and  if .' decidableDrop the witness of proof of a , returning  if  and  if  (with the disproof).( decidableBoolean test if a  is .) decidableBoolean test if a  is .*  !"#$%&'()*# !"  $%&'()1111(c) Justin Le 2018BSD3 justin@jle.im experimental non-portableNone+,-;<=FQSTV]di3#1 decidable+Two-way implication, or logical equivalence2 decidable2 p q is a constraint that p 1 q is  ; that is, you can prove that p is logically equivalent to q.3 decidable3 p q is a constraint that p 4 q is  ; that is, you can prove that p implies q.4 decidablep ==> q is true if q+ is provably true under the condition that p is true.5 decidablep 5 q is a predicate that either p and q are true, but not both.6 decidablecRight-biased "or". In proofs, prioritize a proof of the right side over a proof of the left side.7 decidablebLeft-biased "or". In proofs, prioritize a proof of the left side over a proof of the right side.8 decidablep 8 q is a predicate that either p and q are true.9 decidablep 9 q is a predicate that both p and q are true.: decidableDecide p 9 q based on decisions of p and q.; decidableDecide p 8 q based on decisions of p and q.< decidableDecide p 5 q based on decisions of p and q.= decidableIf q is provable, then so is p 4 q.$This can be used as an easy plug-in   instance for p 4 q if q is  : Hinstance Provable (p ==> MyPred) where prove = proveImplies @MyPred UThis instance isn't provided polymorphically because of overlapping instance issues.> decidableFrom   a<, you can prove anything. Essentially a lifted version of .? decidable# can be proven from all predicates.@ decidableWe cannot have both p and  p.A decidableIf only this worked, but darn overlapping instances. Same for p ==> p ||| q and p &&& q ==> p :( q) ==> instance Provable (p &&& Not p ==> Impossible) where prove = excludedMiddle @p)If p implies q, then not q implies not p.B decidableReverse direction of A. Only possible if q is  ! on its own, without the help of p%, which makes this much less useful.C decidable+Logical double negation. Only possible if p is  .D decidableIf p 9 q is true, then so is p.E decidableIf p 9 q is true, then so is q.F decidableIf p is true, then so is p 8 q.G decidableIf q is true, then so is p 8 q.K decidableL decidableM decidableN decidableO decidableP decidableQ decidableR decidableS decidableT decidableU decidableV decidable"#123456789:;<=>?@ABCDEFG#9:8;765<4=312">?@CABDEFG11418293(c) Justin Le 2018BSD3 justin@jle.im experimental non-portableNone&',-.0;<=>?FQSTV]di[ decidableDTrivially witness an item in the second field of a type-level tuple.] decidable Witness an item in a type-level U by either indicating that it is the "head", or by providing an index in the "tail".` decidable Witness an item in a type-level  j by proving the  is .b decidable Witness an item in a type-level  by proving the  is .d decidable<Witness an item in a type-level list by providing its index.g decidableA g f p is a predicate on a collection as that no a in as satisfies predicate p.h decidablePredicate that a given  as :: f k0 is not empty, and has at least one item in it.i decidablePredicate that a given  as :: f k! is empty and has no items in it.j decidable_Typeclass for a type-level container that you can quantify or lift type-level predicates over.k decidablez, but providing an y.l decidable{, but providing an y.m decidable|, but providing an y.n decidableAn n f p% is a predicate testing a collection  as :: f a for the fact that all items in as satisfy p=. Represents the "forall" quantifier over a given universe.This is mostly useful for its  ,  , and / instances, which lets you lift predicates on p to predicates on n f p.o decidableA o p as! is a witness that the predicate p a is true for all items a in the type-level collection as.r decidableAn r f p% is a predicate testing a collection  as :: f a) for the fact that at least one item in as satisfies p=. Represents the "exists" quantifier over a given universe.This is mostly useful for its   and / instances, which lets you lift predicates on p to predicates on r f p.s decidableA s p as* is a witness that, for at least one item a in the type-level collection as, the predicate p a is true.u decidableu f as# is a predicate that a given input a is a member of collection as.y decidableCA witness for membership of a given item in a type-level collectionz decidableLifts a predicate p on an individual a( into a predicate that on a collection as that is true if and only if any item in as# satisfies the original predicate.&That is, it turns a predicate of kind  k ~> Type into a predicate of kind  f k ~> Type.-Essentially tests existential quantification.{ decidableLifts a predicate p on an individual a( into a predicate that on a collection as that is true if and only if all items in as# satisfies the original predicate.&That is, it turns a predicate of kind  k ~> Type into a predicate of kind  f k ~> Type.+Essentially tests universal quantification.| decidableIf p a is true for all values a in as# under some (Applicative) context h, then you can create an n p as! under that Applicative context h.Can be useful with . (which is basically unwrapping and wrapping n ), or with U (which can express predicates that are either provably true or not provably false).`In practice, this can be used to iterate and traverse and sequence actions over all "items" in as.} decidable~, but providing an y.~ decidableIf p a is true for all values a in as, then we have n p as). Basically witnesses the definition of n. decidable5Extract the item from the container witnessed by the y decidableSplit a  as into a proof that all a in as exist. decidable:Automatically generate a witness for a member, if possible decidable but with access to the index. decidableA  over all items in a collection. k decidablepredicate on value decidablepredicate on collectionl decidablepredicate on value decidablepredicate on collectionm decidablepredicate on value in context decidable"predicate on collection in contextz decidablepredicate on value decidablepredicate on collection{ decidablepredicate on value decidablepredicate on collection| decidablepredicate on value in context decidable"predicate on collection in context} decidablealways-true predicate on value decidable#always-true predicate on collection~ decidablealways-true predicate on value decidable#always-true predicate on collection decidableWitness decidable Collection([\]^_`abcdefghijklmnopqrstuvwxyz{|}~(yujklmdefbc`a]^_[\nopqrstgihz{|~}xwv(c) Justin Le 2018BSD3 justin@jle.im experimental non-portableNone&',-;<=>?FQSTV]di  decidable, but providing an y. decidableLifts a predicate p on an individual a( into a predicate that on a collection as that is true if and only if no item in as# satisfies the original predicate.&That is, it turns a predicate of kind  k ~> Type into a predicate of kind  f k ~> Type. decidable, but providing an y. decidableIf there exists an a s.t. p a , and if p implies q, then there must exist an a s.t. q a. decidable, but providing an y. decidable If for all a we have p a , and if p implies q, then for all a we must also have p a. decidable, but providing an y. decidableIf p implies q under some context h, and if there exists some a such that p a, then there must exist some a such that p q under that context h.h might be something like, say, F, to give predicate that is either provably true or unprovably false.-Note that it is not possible to do this with p a ->  (q a). This is if the p a ->  (q a)< implication is false, there it doesn't mean that there is no a such that q a), necessarily. There could have been an a where p does not hold, but q does. decidable, but providing an y. decidableIf p implies q under some context h, and if we have p a for all a, then we must have q a for all a under context h. decidable, but providing an y. decidable If we have p a for all a, and p a can be used to test for q a, then we can test all as for q a.  decidablepredicate on value decidablepredicate on collection decidablepredicate on value decidablepredicate on collection decidable implication decidable implication decidableimplication in context decidableimplication in context decidableimplication in context decidableimplication in context decidabledecidable implicationglknopqrstz{rstgzknopq{l(c) Justin Le 2018BSD3 justin@jle.im experimental non-portableNone+,-7;<=FSTV]di%  decidable f$ takes a parmaeterized predicate on k (testing for a v1) and turns it into a parameterized predicate on f k (testing for a v). It "lifts" the domain into f.An  f p as# is a predicate taking an argument a and testing if p a ::  k is satisfied for any item in  as :: f k.A  k v tests if a k can create some v. The resulting  (f k) v tests if any k in f k can create some v. decidableA  (f k) k. Parameterized on an  as :: f k8, returns a predicate that is true if there exists any a :: k in as. Essentially h. decidableA constraint that a  k v/ s "selectable". It means that for any input x :: k, we can always find a y :: v that satisfies  P x @@ y. We can "select" that y, no matter what. decidableA constraint that a  k v0 is "searchable". It means that for any input x :: k/, we can prove or disprove that there exists a y :: v that satisfies P x @@ y. We can "search" for that y,, and prove that it can or cannot be found. decidablePre-compose a function to a . Is essentially  ()T, but unfortunately defunctionalization doesn't work too well with that definition. decidable Promote a  v to a  k v, ignoring the k input. decidableFlip the arguments of a . decidableDConvert a parameterized predicate into a predicate on the parameter.A  p is a predicate on p ::  k v that tests a k# for the fact that there exists a v where  k v is satisfied.$Intended as the basic interface for , since it turns a  into a normal , which can have   and   instances.!For some context, an instance of   ( P), where P ::  k v, means that for any input x :: k, we can always find a y :: v such that we have P x  y.5In the language of quantifiers, it means that forall x :: k, there exists a y :: v such that P x  y.For an instance of   ( P), it means that for all x :: k8, we can prove or disprove the fact that there exists a y :: v such that P x  y. decidable A parameterized predicate. See  for more information. decidable$The deciding/searching function for  p.Must be called by applying the :  @p  decidable#The proving/selecting function for  p.Must be called by applying the :  @p (c) Justin Le 2018BSD3 justin@jle.im experimental non-portableNone&',-;<=>?FSTVi= decidableTypeclass representing ys pointing to an a :: kA that can be generated automatically from type-level collection  as :: f k. If GHC knows both the type-level collection and the element you want to find at compile-time, this instance should allow it to find it. Used to help in the instance of  for the u predicate.Example usage: BautoElem :: Index '[1,6,2,3] 2 -- IS (IS IZ) -- third spot And when used with : auto _ $(In [] '[1,6,2,3]) @2 -- IS (IS IZ)  decidable Generate the y pointing to the a ::  in a type-level collection  as :: f k. decidable9Helper "predicate transformer" that gives you an instant  for any   instance.$For example, say you have predicate P that you know is  , and you wish to generate a P @@ x, for some specific x) you know at compile-time. You can use:  _ (AutoProvable P) @x  to obtain a P @@ x.& is essentially the identity function. decidable/Automatically generate a witness for predicate p applied to input a.,Mostly useful for situations where you know a) at compile-time, so you can just write F directly in your source code. The choice is intended to mirror the auto! keyword in languages like Idris.Very close in nature to the Known typeclass in the type-combinators library. decidable)Have the compiler generate a witness for p @@ a.-Must be called using type application syntax:  _ p @a (c) Justin Le 2018BSD3 justin@jle.im experimental non-portableNone&',-;<=>?FQSTV]diP decidableA  f p8 is a predicate that some decidable subset of an input as is true. decidableA  f p  as describes a  decidable" subset of type-level collection as. decidable Create a  from a predicate. decidableTurn a  into a list (or any ) of satisfied predicates.'List is meant to include no duplicates. decidable Restrict a 9 to a single (arbitrary) member, or fail if none exists. decidableConstruct an empty subset. decidableConstruct a full subset decidableTest if a subset is empty. decidable0Combine two subsets based on a decision function decidable0Combine two subsets based on a decision function decidableSubset intersection decidable Subset union decidableSymmetric subset difference decidable;Test if a subset is equal to the entire original collection decidable, but providing an y. decidableMMap a bidirectional implication over a subset described by that implication.HImplication needs to be bidirectional, or otherwise we can't produce a  decidable subset as a result.SafeP      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdeefghiijjklmnopqrstuvvwxyyz{|}~8     (decidable-0.1.1.0-8lmSWbLVfSD77vRVLWzzRPData.Type.PredicateData.Type.Predicate.LogicData.Type.Universe"Data.Type.Predicate.QuantificationData.Type.Predicate.ParamData.Type.Predicate.AutoData.Type.Universe.SubsetPaths_decidable'singletons-2.4.1-CPkrVyNL0Sy7pQw5p6j80uData.Singletons.Decide DisprovedProvedDecisionNotTFunctortmapDFunctordmap ProvableTC DecidableTC DisprovableProvableprove Decidabledecide-->#-->Prove-?>#-?>DecideWitgetWitPMapBoolPredEqualTo ImpossibleEvidentTyPred PredicatedisprovedecideTCproveTCcompImpl decideNot flipDecision mapDecisionforgetDisproof forgetProofisProved isDisproved$fProvablek1.@#@$$$$fProvablek1TyCon$fDecidablek1.@#@$$$$fDecidablek1TyCon$fDecidablekTyCon$fDecidablek1Not$fProvablek1Not<==>EquivImplies==>^^^||^^|||||&&& decideAnddecideOr decideXor proveImplies explosionatomexcludedMiddlecontrapositivecontrapositive'doubleNegation projAndFst projAndSnd injOrLeft injOrRight$fProvablek1&&&$fDecidablek1&&&$fDecidablek1|||$fProvablek1==>$fDecidablek1==>$fProvablek1==>0$fDecidablek1==>0$fProvablek1==>1$fDecidablek1==>1$fProvablek1==>2$fDecidablek1==>2$fProvablek1==>3$fDecidablek1==>3$fProvablek1==>4$fDecidablek1==>4$fProvablek1==>5$fDecidablek1==>5$fProvablek1==>6$fDecidablek1==>6SndNEIndexNEHeadNETailIsRightIsJustIndexIZISNoneNotNullNullUniverse idecideAny idecideAlligenAllAAllWitAll runWitAllAnyWitAnyInElemSym2ElemSym1ElemSym0Elem decideAny decideAllgenAllAigenAllgenAllindexpickElem ifoldMapUni foldMapUni$fDFunctork1fAll$fTFunctork1fAll$fTFunctork1fAny$fProvablefAll$fDecidablefAll$fDecidablefAny$fProvablef==>$fDecidablef==> $fUniverse[]$fUniverseMaybe$fDecidablekTyCon0$fUniverseEither$fDecidablekTyCon1$fUniverseNonEmpty$fDecidablekTyCon2 $fUniverse(,)$fDecidablekTyCon3 $fShowSnd $fShowNEIndex $fShowIsRight $fShowIsJust $fShowIndex idecideNone decideNone ientailAny entailAny ientailAll entailAll ientailAnyF entailAnyF ientailAllF entailAllFidecideEntailAlldecideEntailAllAnyMatchInP Selectable SearchablePPMapConstPPFlipPPFound ParamPredsearchselect$fProvablekFound$fDecidablekFound$fProvablef==>0$fDecidablef==>0$fDecidablefFound$fDecidablefFound0AutoElemautoElem AutoProvableAutoauto $fAutok==>a $fAutok&&&a $fAutokTyCona$fAutokTyCona0$fAutokAutoProvablea$fAutokElemSym1a$fAutoElemkNonEmpty:|a$fAutoElemkNonEmpty:|a0$fAutoElemkEitherRighta$fAutoElemkMaybeJusta$fAutoElemk[]:a$fAutoElemk[]:a0Subset WitSubset runWitSubset makeSubset subsetToList subsetToAny emptySubset fullSubset subsetToNone imergeSubset mergeSubset intersectionunionsymDiff subsetToAll imapSubset mapSubset$fProvablefSubset$fDecidablefSubsetghc-prim GHC.TypesTypeRefutedBoolData.Singletons.Prelude.Base ConstSym1Data.Singletons.Internal@@ApplybaseGHC.BaseMaybeJustNothing Data.VoidabsurdNonEmpty Data.EitherEitherRightData.Functor.IdentityIdentity splitSingSing Data.FoldablefoldMapflip. Alternativeversion getBinDir getLibDir getDynLibDir getDataDir getLibexecDir getSysconfDirgetDataFileName