Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Sprache: Unknown

Columbo aufrufen.sig zum Wurzelverzeichnis wechselnVHDL {VHDL[127] Ada[132] Abap[205]}Datei anzeigen

(* ========================================================================= *)
(* A STORE FOR UNIT THEOREMS                                                 *)
(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License     *)
(* ========================================================================= *)

signature Units =
sig

(* ------------------------------------------------------------------------- *)
(* A type of unit store.                                                     *)
(* ------------------------------------------------------------------------- *)

type unitThm = Literal.literal * Thm.thm

type units

(* ------------------------------------------------------------------------- *)
(* Basic operations.                                                         *)
(* ------------------------------------------------------------------------- *)

val empty : units

val size : units -> int

val toString : units -> string

val pp : units Print.pp

(* ------------------------------------------------------------------------- *)
(* Add units into the store.                                                 *)
(* ------------------------------------------------------------------------- *)

val add : units -> unitThm -> units

val addList : units -> unitThm list -> units

(* ------------------------------------------------------------------------- *)
(* Matching.                                                                 *)
(* ------------------------------------------------------------------------- *)

val match : units -> Literal.literal -> (unitThm * Subst.subst) option

(* ------------------------------------------------------------------------- *)
(* Reducing by repeated matching and resolution.                             *)
(* ------------------------------------------------------------------------- *)

val reduce : units -> Rule.rule

end

[ Original von:0.166Diese Quellcodebibliothek enthält Beispiele in vielen Programmiersprachen. Man kann per Verzeichnistruktur darin navigieren. Der Code wird farblich markiert angezeigt. ]