products/Sources/formale Sprachen/Isabelle/Tools/Metis/src image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: Ordered.sig   Sprache: Unknown

Spracherkennung für: .sig vermutete Sprache: SML {SML[74] Latech[95] Coq[100]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen]

(* ========================================================================= *)
(* ORDERED TYPES                                                             *)
(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License     *)
(* ========================================================================= *)

signature Ordered =
sig

type t

val compare : t * t -> order

(*
  PROVIDES

  !x : t. compare (x,x) = EQUAL

  !x y : t. compare (x,y) = LESS <=> compare (y,x) = GREATER

  !x y : t. compare (x,y) = EQUAL ==> compare (y,x) = EQUAL

  !x y z : t. compare (x,y) = EQUAL ==> compare (x,z) = compare (y,z)

  !x y z : t.
    compare (x,y) = LESS andalso compare (y,z) = LESS ==>
    compare (x,z) = LESS

  !x y z : t.
    compare (x,y) = GREATER andalso compare (y,z) = GREATER ==>
    compare (x,z) = GREATER
*)


end

[ Dauer der Verarbeitung: 0.71 Sekunden  ]