(* Title: HOL/TLA/Memory/RPCMemoryParams.thy Author: Stephan Merz, University of Munich
*)
section \<open>Basic declarations for the RPC-memory example\<close>
theory RPCMemoryParams imports Main begin
type_synonym bit = "bool" (* Signal wires for the procedure interface. Defined as bool for simplicity. All I should really need is
the existence of two distinct values. *)
(* all of these are simple (HOL) types *) typedecl Locs (* "syntactic" value type *) typedecl Vals (* "syntactic" value type *) typedecl PrIds (* process id's *)
end
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
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.
