|
% the booleans are a finite type.
% this theory is useful to discharge TCCs from finiteness proofs for
% composed types such as set[T] = [T -> bool]
%
% Author: Alfons Geser, National Institute of Aerospace
% Date: Jan 2005
booleans_are_finite: THEORY
BEGIN
bool_is_finite_type: LEMMA
is_finite_type[bool]
implies_is_total_order: JUDGEMENT
IMPLIES HAS_TYPE (total_order?[bool])
IMPORTING finite_types[bool], finite_total_orders[bool, IMPLIES]
END booleans_are_finite
¤ Dauer der Verarbeitung: 0.17 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
