support user function names and type designators
Issue 6641 explains several related problems. The basic issue is that in a type designator or in an rte, the user specifies symbols, which may not be fully qualified. These must get resolved somehow. The user might have designated his own predicate function for (satisfies ...) or his own rte tokens defined with with-rte.
This must somehow function independent of the users value of *ns*.
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information