products/sources/formale Sprachen/Coq/ide/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: univ.ml   Sprache: Unknown

%
%
% Purpose : a message with a linear order.
%
%


ordered_message[T: TYPE+, leq: (total_order?[T])]: THEORY

BEGIN

  IMPORTING message[T]

  d1, d2: VAR message

  valid_iff_ord1: LEMMA (valid?(d1) IFF ord(d1) = 1)

  d3: VAR message

  <=(d1, d2): bool =
    IF valid?(d1) & valid?(d2)
      THEN leq(value(d1), value(d2))
      ELSE ord(d1) <= ord(d2)
    ENDIF

  eq_iff: LEMMA d1 = d2 IFF
    (valid?(d1) AND valid?(d2) AND value(d1) = value(d2)) OR
    (ord(d1) = ord(d2) AND ord(d1) /= 1 )

  message_total_order: JUDGEMENT <= HAS_TYPE (total_order?[message[T]])

END ordered_message

[ Verzeichnis aufwärts0.16unsichere Verbindung  Übersetzung europäischer Sprachen durch Browser  ]