[mizar] a puzzling *185

[Jesse Alama <alama@stanford.edu>]

Consider the definition:

definition let p be polyhedron;
  func 0-chain-space(p) equals
  VectSpStr(# 0-chains(p), 0-chain-sum(p), 0-chain-zero(p), 0-chain-scalar-mult(p) #);
  correctness;
end;

I've defined 0-chains(p), 0-chain-sum(p), 0-chain-zero(p), and
0-chain-scalar-mult(p) in such a way that this definition is accepted
without errors.  To my surprise, however, the follow modified
definition is rejected:

definition let p be polyhedron;
  func 0-chain-space(p) -> VectSpStr equals
::>                                       *185
  VectSpStr(# 0-chains(p), 0-chain-sum(p), 0-chain-zero(p), 0-chain-scalar-mult(p) #);
  correctness;
end;

Error 185 is "Unknown structured mode format".  What puzzles me is
that for an earlier structure I was able to successfully declare a
type:

definition
  func F2 -> doubleLoopStr equals
    doubleLoopStr(# {0,1}, add2, prod2, unit2, zero2 #);
  coherence;
end;

What might be going on with my error 185?

Thanks,

Jesse

-- 
Jesse Alama (alama@stanford.edu)
*104: Unknown structure (http://www.mizar.org)