bossLib.namedCases

An application of namedCases_on q [s1, ..., sn] to a goal A ?- P first parses q in the context of the goal to yield a term tm:ty, then uses ty to look up a a so-called "nchotomy" theorem installed in the system database of declared datatypes, then performs a case split on how tm can be constructed. The strings s1, ..., sn designate the names to be used as arguments of the constructor in each case. This yields the goals

    (A, tm = <constr>1 <names>1 ?- P)
     ,...,
    (A, tm = <constr>n <names>n ?- P)

For a datatype with n constructors, n strings are expected to be supplied. If no strings are supplied, the system will use a default naming scheme. If the ith constructor has no arguments, then si should be the empty string. If the ith constructor has k arguments, then si should consist of k space-separated names. In case a name does not need to be specified, an underscore _ or dash - can be supplied, in which case a default name will be conjured up.

In case ty is a product type ty1 # ... # tyi, namedCases_on q [s] will iteratively case split on all product types in ty, thus replacing x:ty by a tuple with i variables, the names of which are taken from s.