The article funct_2.miz contains the following fragment (lines 933 - 937):
-------------------------------
registration let X;
let f,g be quasi_total PartFunc of X,X;
cluster g*f -> quasi_total PartFunc of X,X;
coherence proof X <> {} or X = {}; hence thesis by Th19; end;
end;
-------------------------------
but the current production rule for functorial registration doesn't allow type
expression:
Functorial-Registration =
"cluster" Term-Expression "->" Adjective-Cluster ";" Correctness-Conditions .
It seems this rule must be like the following (though I am not sure about it).
Functorial-Registration =
"cluster" Term-Expression "->" Adjective-Cluster [ Type-Expression] ";"
Correctness-Conditions .
Can anyone confirm it?