One issue can be that if some sort involves multiple type classes, the corresponding class may not have been defined. That is the one advantage of sorts: you can create conjunctions/intersection of type classes on the fly.
Tobias Tjark Weber schrieb: > Hi, > > I noticed that numerous lemmas in HOL that refer to class constants are > stated at the top level (using implicit or explicit sort annotations), > rather than in the corresponding class context (see, for instance, > Compl_lessThan in HOL/SetInterval.thy). If I am not mistaken, this > means the corresponding lemma is not available in the context of the > class, which seems unfortunate. Is this merely a legacy issue, or are > there genuine reasons for stating these lemmas with sort annotations? > > Kind regards, > Tjark > > _______________________________________________ > isabelle-dev mailing list > [email protected] > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
