Re: [mizar] a puzzling *185

[Jesse Alama <alama@stanford.edu>]

Jesse Alama <alama@stanford.edu> writes:

> 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?

I forgot to include another puzzling fact: the definition

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

is accepted without errors.  So there's a difference between saying
that 0-chain-space(p) is a VectSpStr and saying that it is a LoopStr.
What is that difference?

Thanks,

Jesse

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