Add some compiler macros that let us prune some unreachable branches in the theorem-prover, when argument values are known at compile time.
Other improvements for compilation, specifically on SBCL:
Add verify-type, a macro that is like check-type, but that does not have a restart. The restart was confusing SBCL's type-checker by making it think that the type of some variables was unknown. Replaced by simply erroring out.
Add some compiler macros that let us prune some unreachable branches in the theorem-prover, when argument values are known at compile time.
Other improvements for compilation, specifically on SBCL:
Add
verify-type, a macro that is likecheck-type, but that does not have a restart. The restart was confusing SBCL's type-checker by making it think that the type of some variables was unknown. Replaced by simply erroring out.Fix use of old "SHOP2" package name.
Replace
assertwithunless+error.