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

Re: [mizar] Isn't "Subset of" the same as "Element of bool"?

Grzegorz Bancerek wrote:

Hi,

Freek Wiedijk wrote:


  definition
   let B be set;
   let A be Subset of B;
   redefine func bool A -> Subset of bool B;
   coherence by ZFMISC_1:79;
  end;


Expandable definitions are "static", i.e., any redefinition of
constructors which are given after "is" has no impact on
identification. They are stored in terms of constructors and
no any connection with notation is recognized.
So  Subset of A is identified (according to MML Query)
   SUBSET_1:mode 1(ZFMISC_1:func 1(A))
even if   bool A is identified now as
   NEWTEXT:func 1(A)


Ops, after Freek's redefinition "bool A" is identified as
   NEWTEXT:func 1(B,A)
with equality with
   ZFMISC_1:func 1(A)

Grzegorz