Quelle Closure_Set.thy

Sprache: Isabelle

(* Title: Containers/Closure_set.thy
Author: Andreas Lochbihler, KIT *)

theory Closure_Set imports Equal begin

section ‹Sets implemented as Closures›

context equal_base begin

definition fun_upd :: "('a ==> 'b) ==> 'a ==> 'b ==> 'a ==> 'b"
where fun_upd_apply: "fun_upd f a b a' = (if equal a a' then b else f a')"

end

lemmas [code] = equal_base.fun_upd_apply
lemmas [simp] = equal_base.fun_upd_apply

lemma fun_upd_conv_fun_upd: "equal_base.fun_upd (=) = fun_upd"
by(simp add: fun_eq_iff)

end

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.8 Sekunden (vorverarbeitet am 2026-06-13) ¤

Wurzel

Suchen

NIST Cobol Testsuite

Haftungshinweis

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 und die Messung sind noch experimentell.