[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] a puzzling *185

Hi,

On Fri, 26 Jan 2007, Jesse Alama wrote:


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?
What makes the difference is the 'over' argument (the underlying field of a vector space) which is used in the notation of VectSpStr, hence the *185 error. 

Best,

Adam Naumowicz

======================================================================
Department of Applied Logic            fax. +48 (85) 745-7662
Institute of Computer Science          tel. +48 (85) 745-7559 (office)
University of Bialystok                e-mail: adamn@mizar.org
Sosnowa 64, 15-887 Bialystok, Poland   http://math.uwb.edu.pl/~adamn/
======================================================================