!%W+      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~      !"#$%&'()*(c) Justin Le 2018BSD3 justin@jle.im experimental non-portableNone,-./8=>?HSUVX_fk2 decidable f as# is a predicate that a given input a is a member of collection as. 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: 1 :: , a -> T a Is essentially , except with type constructors k -> +6 instead of matchable type-level functions (that are k ~> +). Useful because 1> doesn't require anything fancy like TypeApplications to use.hAlso is in this library for compatiblity with "traditional" predicates that are GADT type constructors. decidableIf  T :: k -> + is a type constructor, then  T is a constraint that T8 is "decidable", in that you have a canonical function: 0 :: , a ->  (T a) Is essentially , except with type constructors k -> +5 instead of matchable type-level functions (that are k ~> +). Useful because 0> doesn't require anything fancy like TypeApplications to use.hAlso is in this library for compatiblity with "traditional" predicates that are GADT type constructors. decidable p is a constraint that p can be disproven. decidableuA typeclass for provable predicates (constructivist tautologies). In some context, these are also known as "views".,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".,We can call a type a view if, for any input a , there is some constructor of p @@ a% that can we can use to "categorize" a.~This typeclass associates a canonical proof function for every provable predicate, or a canonical view function for any view.It confers two main advatnages: The proof functionview for every predicate(view 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) (or a canonical view function for view p). Note that  is ambiguously typed, so you always\ need to call by specifying the predicate you want to prove using TypeApplications syntax:  @MyPredicate See 1 and B for a version that isn't ambiguously typed, but only works when p is a type constructor. 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 See 0 and B for a version that isn't ambiguously typed, but only works when p is a type constructor. 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 p9; in some contexts, also called a "view function". 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. * :: k -> . k + decidableThe always-false predicateCould also be defined as / Void&, but this defintion gives us a free  instance. + :: . k , 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 0 is 1, the singleton library's type-level function application for mathcable functions). In some contexts, this is also known as a dependently typed "view".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 1N instance, to specify the type of the -- witnesses of that predicate instance 1 (Not p) a = (p 0 a) -> 2 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 :: . k instance Apply Evident a = , a #And the "and" predicate combinator: Xdata (&&&) :: Predicate k -> Predicate k -> Predicate k instance Apply (p &&& q) a = (p 0 a, q 0 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 0 decidable$The canonical deciding function for  t.Note that because tn must be an injective type constructor, you can use this without explicit type applications; the instance of ' can be inferred from the result type.1 decidable#The canonical proving function for  t.Note that because tn must be an injective type constructor, you can use this without explicit type applications; the instance of ' can be inferred from the result type.2 decidableCompose two implications.3 decidableDecide  p based on decisions of p.4 decidable2Flip the contents of a decision. Turn a proof of a into a disproof of not-a.JNote that this is not reversible in general in constructivist logic See  for a situation where it is.5 decidableMap over the value inside a .6 decidable Converts a  to a 3$. Drop the witness of disproof of a , returning 4 if  (with the proof) and 5 if .7 decidableDrop the witness of proof of a , returning 5 if  and 4 if  (with the disproof).8 decidableBoolean test if a  is .9 decidableBoolean test if a  is .: decidableMHelper function for a common pattern of eliminating the disproved branch of  to certaintify the proof.; decidableChange the target of a -( with a contravariant mapping function.= decidable> decidable? decidable@ decidableA decidableB decidableE decidableF decidableG decidableH decidableI decidableJ decidable- !"#$%&'()*+,-./0123456789:;-.%&'-,*)+(3! /12$#"045:6789;1 1"1#1(c) Justin Le 2018BSD3 justin@jle.im experimental non-portableNone,-.=>?HPSUVX_k'U decidable+Two-way implication, or logical equivalenceV decidableV p q is a constraint that p U q is ; that is, you can prove that p is logically equivalent to q.W decidableW p q is a constraint that p X q is ; that is, you can prove that p implies q.X decidablep ==> q is true if q+ is provably true under the condition that p is true.Y decidablep Y q is a predicate that either p and q are true, but not both.Z decidablecRight-biased "or". In proofs, prioritize a proof of the right side over a proof of the left side.[ decidablebLeft-biased "or". In proofs, prioritize a proof of the left side over a proof of the right side.\ decidablep \ q is a predicate that either p and q are true.] decidablep ] q is a predicate that both p and q are true.^ decidableDecide p ] q based on decisions of p and q._ decidableDecide p \ q based on decisions of p and q.Prefers p over q.` decidableDecide p Y q based on decisions of p and q.a decidableIf q is provable, then so is p X q.$This can be used as an easy plug-in  instance for p X q if q is : Hinstance Provable (p ==> MyPred) where prove = proveImplies @MyPred UThis instance isn't provided polymorphically because of overlapping instance issues.b decidableFrom +  a<, you can prove anything. Essentially a lifted version of 6.c decidable,# can be proven from all predicates.d decidableWe cannot have both p and  p.!(Renamed in v0.1.4.0; used to be excludedMiddle)e decidable)If p implies q, then not q implies not p.f decidableReverse direction of e. Only possible if q is ! on its own, without the help of p%, which makes this much less useful.g decidable+Logical double negation. Only possible if p is .lThis is because in constructivist logic, not (not p) does not imply p. However, p implies not (not p) (see i-), and not (not (not p)) implies not p (see h)h decidable9In constructivist logic, not (not (not p)) implies not p.i decidable/In constructivist logic, p implies not (not p).j decidableIf p ] q is true, then so is p.k decidableIf p ] q is true, then so is q.l decidableIf p is true, then so is p \ q.m decidableIf q is true, then so is p \ q.p decidablePrefers p over q.q decidabler decidables decidablet decidableu decidablev decidablew decidablex decidabley decidablez decidable{ decidable| decidable} decidable+,23UVWXYZ[\]^_`abcdefghijklm,+3]^\_[ZY`XaWUV2bcdghiefjklmU1X1\2]3(c) Justin Le 2018BSD3 justin@jle.im experimental non-portableNone&'-./124567=?HSUVX_fk decidable Test that an 7 is 8 decidable Test that an 7 is 9 decidable Test that a 3 is 5. decidable Test that a 3 is 4. decidableA  f p is a predicate on a collection as that at least one a in as does not satisfy predicate p. decidableA  f p is a predicate on a collection as that no a in as satisfies predicate p. decidablePredicate that a given  as :: f k0 is not empty, and has at least one item in it. decidablePredicate that a given  as :: f k! is empty and has no items in it. decidable_Typeclass for a type-level container that you can quantify or lift type-level predicates over. decidable, but providing an . decidable, but providing an . decidableAn  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  f p. decidableA  p as! is a witness that the predicate p a is true for all items a in the type-level collection as. decidableAn  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  f p. decidableA  p as* is a witness that, for at least one item a in the type-level collection as, the predicate p a is true. 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. decidableSplit a , as into a proof that all a in as exist. decidable:Automatically generate a witness for a member, if possible decidable, but providing an . decidableIf p a is true for all values a in as, then we have  p as). Basically witnesses the definition of . decidableSplit a , as into a proof that all a in as exist. decidableThe single-pointed universe. decidablepredicate on value decidablepredicate on collection decidablepredicate on value decidablepredicate on collection decidablepredicate on value decidablepredicate on collection decidablepredicate on value decidablepredicate on collection decidablealways-true predicate on value decidable#always-true predicate on collection decidablealways-true predicate on value decidable#always-true predicate on collection+ + (c) Justin Le 2018BSD3 justin@jle.im experimental non-portableNone -.HSUVX_k4 decidable, but providing an . 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 . 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 . 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 . 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, 3F, 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 . 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 . 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. decidable5It is impossible for any value in a collection to be +. decidableIf any a in as does not satisfy p, then not all a in as satisfy p. decidable If not all a in as satisfy p#, then there must be at least one a in as that does not satisfy p . Requires  p# in order to locate that specific a. decidableIf p is false for all a in as , then no a in as satisfies p. decidableIf no a in as satisfies p, then p is false for all a in as . Requires  p# to interrogate the input disproof. decidableoIf something is true for all xs, then it must be true for at least one x in xs, provided that xs is not empty.  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 implication(c) Justin Le 2018BSD3 justin@jle.im experimental non-portableNone&',-.=>?HUVX_k~[ decidableConjunction on two s, with appropriate  and  instances. decidableDisjunction on two s, with appropriate 5 instance. Priority is given to the left predicate. 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 . decidableIf T :: k -> v -> + is a type constructor, then  T is a constraint that T9 is "selectable", in that you have a canonical function:  :: , a ->  v ( T x) That is, given an x :: k , we can always find a y :: k that satisfies T x y.Is essentially , except with type constructors k -> +5 instead of matchable type-level functions (that are k ~> +). Useful because > doesn't require anything fancy like TypeApplications to use. decidableIf T :: k -> v -> + is a type constructor, then  T is a constraint that T9 is "searchable", in that you have a canonical function:  :: , x ->  ( v ( T x)) That, given an x :: k!, we can decide whether or not a y :: v exists that satisfies T x y.Is essentially , except with type constructors k -> +5 instead of matchable type-level functions (that are k ~> +). Useful because > doesn't require anything fancy like TypeApplications to use. 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 , but on the "value" side. decidablePre-compose a function to a . Is essentially : (;)T, but unfortunately defunctionalization doesn't work too well with that definition. decidableConvert a normal '->'/ type constructor taking two arguments into a .  :: (k -> v -> +) ->  k v  decidableFound ( t) @@ x is true if x, was made using the unary type constructor t. For example: :type IsJust = (Found (IsTC 'Just) :: Predicate (Maybe v)) makes a predicate where  IsJust @@ x is true if x is 4, and false if x is 5. For a more general version, see  The kind of  is:  :: (v -> k) ->  k v  ( t) :: . k Applied to specific things:  '4 ::  (Maybe v) v  ( 'Just') :: . (Maybe v)  decidableFound ( f) @@ x0 is true if there exists some value when, with f applied to it, is equal to x.See # for a useful specific application.  :: (v ~> k) ->  k v  ( f) :: . k  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  cannot exist a v where  k v is satisfied. That is,  P @@ x is satisfied if no y :: v can exist where P x @@ y is satisfied.!For some context, an instance of  ( P), where P ::  k v, means that for any input x :: k, we can always reject any y :: v that claims to satisfy P x @@ y.5In the language of quantifiers, it means that forall x :: k, there does not exist a y :: v such that P x @@ y.For an instance of  ( P), it means that for all x :: k@, we can prove or disprove the fact that there does not exist a y :: v such that P x @@ y. 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.FBecause this is ambiguously typed, it must be called by applying the :  @p See  and B for a version that isn't ambiguously typed, but only works when p is a type constructor. decidable#The proving/selecting function for  p.FBecause this is ambiguously typed, it must be called by applying the :  @p See  and B for a version that isn't ambiguously typed, but only works when p is a type constructor. decidable%The canonical selecting function for  t.Note that because tn must be an injective type constructor, you can use this without explicit type applications; the instance of ' can be inferred from the result type. decidable%The canonical selecting function for  t.Note that because tn must be an injective type constructor, you can use this without explicit type applications; the instance of ' can be inferred from the result type. decidable f is basically  ( f). decidable f is basically  ( f).(c) Justin Le 2018BSD3 justin@jle.im experimental non-portableNone,-.=>?@AHUVX_fk$  decidableAn  p a constraint means that p @@ a. can be proven to not be true at compiletime. decidableHelper class for deriving  instances for  predicates; each C instance is expected to implement these if possible, to get free  instaces for their  predicates.Also helps for   predicates and    predicates. decidable Generate an ) for a given predicate over all items in as. decidableTypeclass representing s 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  predicate.Example usage:  :: 1 '[1,6,2,3] 2 -- IS (IS IZ) -- third spot And when used with :  @_ @(! [] '[1,6,2,3]) @2 -- IS (IS IZ)  decidable Generate the  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:  @_ @( 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.^Admittedly this interface is a bit clunky and ad-hoc; at this point you can just try writing  in your code and praying that it works. You always have the option, of course, to just manually write proofs. If you have any inference rules to suggest, feel free to submit a PR!An important limitation of } is the Haskell type system prevents "either-or" constraints; this could potentially be implemented using compiler plugins.JOne consequence of this is that it is impossible to automatically derive  f p and  ( f p).0For these, the compiler needs help; you can use  and  for these situations. decidable)Have the compiler generate a witness for p @@ a.-Must be called using type application syntax:  _ p @a  decidable A version of P that "just works" with type inference, if the predicate is a type constructor. decidable Disprove p @@ a at compiletime.  @_ @p @a ::  p 0 a  decidableHelper function to generate an  f p! if you can pick out a specific a in as1 where the predicate is provable at compile-time.7This is used to get around a fundamental limitation of  as a Haskell typeclass. decidableHelper function to generate a  ( f p)! if you can pick out a specific a in as4 where the predicate is disprovable at compile-time.7This is used to get around a fundamental limitation of  as a Haskell typeclass. decidable decidable decidable decidable decidable decidable decidable decidable decidable decidable decidable decidable decidable decidable decidable decidable  decidable  decidable  decidable decidable (c) Justin Le 2018BSD3 justin@jle.im experimental non-portableNone -.HSUVXkd 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$ decidableSubset union (left-biased)% decidableSymmetric subset difference& decidable;Test if a subset is equal to the entire original collection' decidable(, but providing an .( 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. !"#$%&'(#$%"!('&  Safe2=>?@ABCDE                   !"#$%&'()*+,-./00123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~      !"#$%&'()*+,-./01 23 4/05 67 28 29:;<:=>:=?:=@:;A:BC:BD:BE:FG:FH:FI J K L M N O P QRdecidable-0.2.1.0-inplaceData.Type.PredicateData.Type.UniverseData.Type.Predicate.Logic"Data.Type.Predicate.QuantificationData.Type.Predicate.ParamData.Type.Predicate.AutoData.Type.Universe.SubsetdoubleNegationPaths_decidableQsingletons-2.5.1-9b65ff6c668ee748f6dbc92feb194b6d1abb0b7c18c1d79e94d59d6ebdd0cc09Data.Singletons.DecideDecisionYfunctor-products-0.1.0.0-d3233694214eee57121f27ffa88c6aa42c298624c8014af07880bdb0847589d0Data.Type.Functor.ProductElemISIZIndexIJustIRightNETailNEHeadNEIndexISndIId IIdentity DisprovedProvedInNotTFunctortmapDFunctordmap ProvableTC DecidableTC DisprovableProvableprove Decidabledecide-->#-->Prove-?>#-?>DecideWitgetWitPMapBoolPredEqualTo ImpossibleEvidentTyPred PredicatedisprovedecideTCproveTCcompImpl decideNot flipDecision mapDecisionforgetDisproof forgetProofisProved isDisproved elimDisproof mapRefuted$fProvablek1.@#@$$$$fProvable(,)TyCon$fProvableEitherTyCon$fProvableIdentityTyCon$fProvableNonEmptyTyCon$fProvableMaybeTyCon$fProvable[]TyCon$fProvablek1TyCon$fDecidablek1.@#@$$$$fDecidable(,)TyCon$fDecidableEitherTyCon$fDecidableIdentityTyCon$fDecidableNonEmptyTyCon$fDecidableMaybeTyCon$fDecidable[]TyCon$fDecidablek1TyCon$fDecidablekTyCon$fDecidablek1Not$fProvablek1Not$fDecidablekElemSym1$fDecidablekElemSym10$fDecidablekElemSym11$fDecidablekElemSym12$fDecidablekElemSym13$fDecidablekElemSym14<==>EquivImplies==>^^^||^^|||||&&& decideAnddecideOr decideXor proveImplies explosionatomcomplementationcontrapositivecontrapositive'tripleNegation negateTwice projAndFst projAndSnd injOrLeft injOrRight$fProvablek1&&&$fDecidablek1&&&$fDecidablek1|||$fProvablek1==>$fProvablek1==>0$fDecidablek1==>$fProvablek1==>1$fDecidablek1==>0$fProvablek1==>2$fDecidablek1==>1$fProvablek1==>3$fDecidablek1==>2$fProvablek1==>4$fDecidablek1==>3$fProvablek1==>5$fDecidablek1==>4$fProvablek1==>6$fDecidablek1==>5$fProvablek1==>7$fDecidablek1==>6IsLeftIsRight IsNothingIsJustNotAllNoneNotNullNullUniverse idecideAny idecideAllallProdprodAllAllWitAll runWitAllAnyWitAny decideAny decideAll splitSingpickElemigenAllgenAllsingAll$fUniverseIdentity $fUniverse(,)$fUniverseNonEmpty$fUniverseEither$fUniverseMaybe $fUniverse[]$fDFunctork1fAll$fTFunctork1fAll$fTFunctork1fAny$fProvablefAll$fDecidablefAll$fDecidablefAny$fProvablef==>$fDecidablef==> idecideNone decideNone ientailAny entailAny ientailAll entailAll ientailAnyF entailAnyF ientailAllF entailAllFidecideEntailAlldecideEntailAll anyImpossible anyNotNotAll notAllAnyNot allNotNone noneAllNotallToAnyAndPOrPAnyMatchInP SelectableTC SearchableTC Selectable SearchablePPMapVPPMapTyPPIsTCEqByConstPPFlipPPNotFoundFound ParamPredsearchselectsearchTCselectTC notNullInP inPNotNull$fProvablekFound$fDecidablekFound$fProvablef==>0$fDecidablef==>0$fDecidablefFound$fDecidablefFound0$fDecidablek1Found$fProvablek1Found$fDecidablek1Found0AutoNotAutoAllautoAllAutoElemautoElem AutoProvableAutoautoautoTCautoNotautoAny autoNotAll$fAutoIdentityTyConas$fAuto(,)TyConas$fAutoEitherTyConas$fAutoNonEmptyTyConas$fAutoMaybeTyConas$fAuto[]TyConas$fAutok.@#@$$$a $fAutokNota $fAutokFounda$fAutoIdentityAnyIdentity$fAuto(,)Any(,)$fAutoNonEmptyAny:|$fAutoEitherAnyRight$fAutoMaybeAnyJust $fAuto[]Any: $fAutok==>a $fAutok&&&a $fAutokTyCona $fAutokNota0$fAutokTyCona0$fAutokAutoProvablea$fAutokElemSym1a$fAutoElemkIdentityIdentitya$fAutoElemk(,)(,)a$fAutoElemkNonEmpty:|a$fAutoElemkNonEmpty:|a0$fAutoElemkEitherRighta$fAutoElemkMaybeJusta$fAutoElemk[]:a$fAutoElemk[]:a0 $fAutofNotas $fAutofNotas0 $fAutofAllas$fAutoAllaIdentitypIdentity$fAutoAllk(,)p(,)$fAutoAllaNonEmptyp:|$fAutoAllbEitherpRight$fAutoAllkEitherpLeft$fAutoAllaMaybepJust$fAutoAllkMaybepNothing$fAutoAlla[]p:$fAutoAllk[]p[] $fAutokNota1Subset WitSubset runWitSubset makeSubset subsetToList subsetToAny emptySubset fullSubset subsetToNone imergeSubset mergeSubset intersectionunionsymDiff subsetToAll imapSubset mapSubset$fProvablefSubset$fDecidablefSubsetghc-prim GHC.TypesTypeData.Singletons.InternalSingRefutedBoolData.Singletons.Prelude.Base ConstSym1@@Applybase Data.VoidVoid GHC.MaybeMaybeJustNothingabsurd Data.EitherEitherLeftRightGHC.Baseflip. Alternativeversion getBinDir getLibDir getDynLibDir getDataDir getLibexecDir getSysconfDirgetDataFileName