List of type prescription rules for the proofs generated by ATC.
These should be probably re-organized by their purpose rather than by their kind (i.e. type prescriptions).
In the dynamic semantics, the execution of statements and other entities returns mv values, which logically satisfy consp; the negated application of consp to those execution functions comes up in certain subgoals, so a simple way to discharge those subgoals is to use the type prescription rules for those execution functions.
We also need rules about the constructors of C integer values and the C functions that represent C operations and conversions, including array read operations.
Definition:
(defconst *atc-type-prescription-rules* '((:t exec-expr-call-or-pure) (:t exec-fun) (:t exec-stmt) (:t exec-block-item) (:t exec-block-item-list) (:t schar-from-integer) (:t uchar-from-integer) (:t sshort-from-integer) (:t ushort-from-integer) (:t sint-from-integer) (:t uint-from-integer) (:t slong-from-integer) (:t ulong-from-integer) (:t sllong-from-integer) (:t ullong-from-integer)))