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

Re: [mizar] unused loci again


Hi Jesse,
I think that what you ask cannot be done in current Mizar. The requirement to "use all loci" is there in order to instantiate the dependent types properly, so that the types of terms could be easily computed in a bottom-up manner. Without that, Mizar has no clue how to instantiate X.
The type-checking algo would have to be changed (probably quite significantly) for this, to proceed also in a top-down manner. 

Josef


On Tue, 10 Jun 2008, Jesse Alama wrote:


I'd like the term {} to have the type `Element of bool X', for every set
X.  How might one express this in mizar?  Registrations apparently won't
do:

 registration
   let X be set;
   cluster
     {} -> Element of bool X;
 ::>                     *100
   coherence;
 end;

Nor can I redefine the term:

 definition
   let X be set;
   redefine func {} -> Element of bool X;
 ::>              *100
   coherence;
 end;

I'm aware of ways to get around this, such as explicitly typing the term
as "{}(X)".  Another approach is to give a name to the empty set with
a statement like

 reconsider emptyset = {} as Element of bool X by sometheorem;

But, if possible, I'd like to stick with the syntatically nice approach
of using just the bare "{}".  Any ideas?