Use this type to filter conditions when computing objects of certain type:

All the functions

$\mathrm{indets}\left(F\left(G\left(x\,y\right)\,z\right)H\left(x\right)\,'\mathrm{function}'\right)$

$\left\{F\left(G\left(x\,y\right)\,z\right)\,G\left(x\,y\right)\,H\left(x\right)\right\}$

Only the functions having y

$\mathrm{indets}\left(F\left(G\left(x\,y\right)\,z\right)H\left(x\right)\,'\mathrm{And}\left(\mathrm{function}\,\mathrm{satisfies}\left(f\mapsto \mathrm{has}\left(f\,y\right)\right)\right)'\right)$

$\left\{F\left(G\left(x\,y\right)\,z\right)\,G\left(x\,y\right)\right\}$

Only the functions having y and not having z

$\mathrm{indets}\left(F\left(G\left(x\,y\right)\,z\right)H\left(x\right)\,'\mathrm{And}\left(\mathrm{function}\,\mathrm{satisfies}\left(f\mapsto \mathrm{has}\left(f\,y\right)\mathbf{and}\mathbf{not}\mathrm{has}\left(f\,z\right)\right)\right)'\right)$

$\left\{G\left(x\,y\right)\right\}$

Use this mechanism to introduce local types within module or procedure bodies. Note that NumberTheory[IsSquareFree] returns true or false when applied to some arguments

$m≔\mathbf{module}\left(\right)\mathrm{\_export}\left(\mathrm{sqrfree}\right)\;\mathrm{sqrfree}≔\'\mathrm{satisfies}\'\left(x\→\mathrm{type}\left(x\,\'\mathrm{odd}\'\right)\,\mathrm{NumberTheory}\[\'\mathrm{IsSquareFree}\'\]\right)\mathbf{end\; module}\:$

Observe that, unlike global type names, which should always be quoted to protect against unwanted evaluation, a local type defined in this way must not be quoted.

For example, the following example cannot have quotes, that is, $\'m:-\mathrm{sqrfree}\'$.

$\mathrm{type}\left(7\,m:-\mathrm{sqrfree}\right)$

$\mathrm{true}$

The global space of names (including the global name sqrfree) remains distinct and so the definition of type m:-sqrfree does not imply the existence of a sqrfree type

$\mathrm{type}\left(7\,\mathrm{sqrfree}\right)$

Error, type `sqrfree` does not exist

Giving predicates in certain order, they are evaluated in that order

$\mathrm{map}\left(\mathrm{type}\,\left[0\,1\,2\right]\,'\mathrm{And}'\left('\mathrm{integer}'\,'\mathrm{satisfies}'\left(s\mapsto \mathrm{evalb}\left(s\ne 0\right)\,s\mapsto \mathrm{type}\left(\frac{1}{s}\,'\mathrm{integer}'\right)\right)\right)\right)$

$\left[\mathrm{false}\,\mathrm{true}\,\mathrm{false}\right]$

While constructing predicates (the procedures testing whether a condition is satisfied), the condition being tester may lead to an error, for example, because the test produces a division by zero.

$\mathrm{map}\left(\mathrm{type}\,\left[0\,1\,2\right]\,'\mathrm{And}'\left('\mathrm{integer}'\,'\mathrm{satisfies}'\left(s\mapsto \mathrm{type}\left(\frac{1}{s}\,'\mathrm{integer}'\right)\right)\right)\right)$

Error, (in unknown) numeric exception: division by zero

You can prevent these situations adding more predicates, taking care of the exceptional cases before the predicate which returns an error is considered

$\mathrm{map}\left(\mathrm{type}\,\left[0\,1\,2\right]\,'\mathrm{And}'\left('\mathrm{integer}'\,'\mathrm{satisfies}'\left(s\mapsto \mathrm{is}\left(s\ne 0\right)\,s\mapsto \mathrm{type}\left(\frac{1}{s}\,'\mathrm{integer}'\right)\right)\right)\right)$

$\left[\mathrm{false}\,\mathrm{true}\,\mathrm{false}\right]$

You can use And, Or, Xor, Implies, Not constructions to make them more readable or to have full control of the evaluation rules when constructing your types - these constructions do not automatically evaluate to true or false.

$\mathrm{condition}≔f\mapsto \mathrm{And}\left(\mathrm{type}\left(f\,\mathrm{function}\right)\,\mathrm{Not}\left(\mathrm{hastype}\left(\frac{f}{\exp \left(1\right)}\,\mathrm{function}\right)\right)\right)$

$\mathrm{condition}≔f\mapsto \mathrm{type}\left(f\,\mathrm{function}\right)\wedge \neg \mathrm{hastype}\left(\frac{f}{\ⅇ}\,\mathrm{function}\right)$

$\mathrm{type}\left(\exp \left(2\right)\,\mathrm{satisfies}\left(\mathrm{condition}\right)\right)$

$\mathrm{false}$

$\mathrm{type}\left(\exp \left(1\right)\,\mathrm{satisfies}\left(\mathrm{condition}\right)\right)$

$\mathrm{true}$