It's only limited in such that you must be able to express the rule using the Shen lisp language. The datatypes are sequents, essentially propositions, that the

It's only limited in such that you must be able to express the rule using the Shen lisp language. The datatypes are sequents, essentially propositions, that the type checker attempts to prove true. For example, I could define odd integers like this: (datatype odd-integer if (integer? X) if (odd? X) ________________ X : odd-integer;)