|
finite_total_orders[T: TYPE+, <=: (total_order?[T])]: THEORY
BEGIN
ASSUMING
finite_type: ASSUMPTION is_finite_type[T]
ENDASSUMING
IMPORTING finite_orders[T], total_lattices[T, <=]
% subsumed :)
% leq_is_a_complete_lattice: JUDGEMENT
% <= HAS_TYPE (complete_lattice?[T])
END finite_total_orders
¤ Dauer der Verarbeitung: 0.25 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
