(* Author: Stefan Berghofer, Lukas Bulwahn, TU Muenchen *)
section‹Simple example for table-based implementation of the reflexive transitive closure›
theory Transitive_Closure_Table_Ex imports"HOL-Library.Transitive_Closure_Table" begin
datatype ty = A | B | C
inductive test :: "ty → ty → bool" where "test A B"
| "test B A"
| "test B C"
text‹Invoking with the predicate compiler and the generic code generator›
code_pred test .
values "{x. test** A C}"
values "{x. test** C A}"
values "{x. test** A x}"
values "{x. test** x C}"
value [nbe] "test** A C" value [nbe] "test** C A"
end
Messung V0.5 in Prozent
¤ 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.0.13Bemerkung:
(vorverarbeitet am 2026-08-25)
¤
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.
