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

[mizar] definitions, vocabularies, and findvoc

Hello,

The abstract of QC_LANG3 contains the definition:

 definition let p;
  func Fixed p -> Element of bool fixed_QC-variables equals
:: QC_LANG3:def 7
  Vars(p,fixed_QC-variables);
 end;

When I run `findvoc Fixed', QC_LANG3 is among the results:

FindVoc, Mizar Ver. 7.0.08 (Darwin/FPC)
Copyright (c) 1990,2004 Association of Mizar Users
vocabulary: QC_LANG3
OFixed  128

vocabulary: TREES_9
OFixedSubtrees 

vocabulary: WAYBEL22
OFixedUltraFilters 

CQ_LANG3's abstract also contains the definition:

 definition let p;
  func Free p -> Element of bool free_QC-variables equals
:: QC_LANG3:def 6
  Vars(p,free_QC-variables);
 end;

However, the output of `findvoc Free' doesn't mention QC_LANG3:

FindVoc, Mizar Ver. 7.0.08 (Darwin/FPC)
Copyright (c) 1990,2004 Association of Mizar Users
vocabulary: FREEALG
OFreeOpNSG 
OFreeOpSeqNSG 
OFreeUnivAlgNSG 
OFreeGenSetNSG 
OFreeOpZAO 
OFreeOpSeqZAO 
OFreeUnivAlgZAO 
OFreeGenSetZAO 

vocabulary: MSAFREE
OFreeSort 
OFreeOper 
OFreeMSA 
OFreeGen 

vocabulary: MSAFREE2
OFreeEnv 

vocabulary: OSAFREE
OFreeOSA 
OOSFreeGen 

vocabulary: WAYBEL22
Ris_FreeGen_set_of 

vocabulary: ZF_MODEL
OFree  72

What explains the difference between Fixed and Free?  Why is QC_LANG3
mentioned in the output of `findvoc Fixed' but not in the output of
`findvoc Free'?

Warm regards,



Jesse