[mizar] Soft Types

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

Dear Freek,

I still try to understand your paper on soft types and I read it again 
(and again). There is a small mistake. Adjectives have arguments, only 
they are always hidden. E.g. if you write
        let R be Relation of A,B;
            R is onto;
('onto' is an adjective in Mizar :-) )

'onto' has two arguments. So, it is rather
        onto(A,B)
It should have only one, of course (B), we work on it. So you should put
't' with arrow after it. So, attributes are constructors like 
predicates, functors or modes. They take a list of terms and create an 
adjective.

All the best,
Andrzej