(This comes from VECTSP_4.) I have a registration
(**) registration let p be polyhedron;
cluster 0-circuit-space(p) -> VectSp of F2;
coherence by <some theorem>;
end;
So 0-circuit-space(p) has type VectSp of F2. But, to my surprise, it
didn't automatically get the adjectives in (*).
No, it doesn't register anything - please remember that term registrations
like this one do not register types for the term specified, only attributes.
The registration in general has the form:
cluster <term> -> adj_1 adj_2 ... adj_n [<type>];
where the optional <type> means only that if <term> already widens to that
<type>, the adjectives adj_1 etc are registered for the <term>.
In your case the list of attributes is just empty, so the registration does
nothing! It seems this new syntax extension which allows to include types in
registrations is very misleading, as people tend to confuse it with
redefinitions.