(* Author: Florian Haftmann, TU Muenchen *) section ‹ A huge collection of equations to generate code from› theory Candidatesimports "HOL-Library.Library" "HOL-Library.Sorting_Algorithms" "HOL-Library.Subseq_Order" "HOL-Library.RBT" "HOL-Data_Structures.Tree_Map" "HOL-Data_Structures.Tree_Set" "HOL-Computational_Algebra.Computational_Algebra" "HOL-Computational_Algebra.Polynomial_Factorial" "HOL-Number_Theory.Eratosthenes" "HOL-Examples.Records" "HOL-Examples.Gauss_Numbers" begin setup ‹ Codegenerator_Test.drop_partial_term_of› text ‹ Simple example for the predicate compiler.› inductive sublist :: "'a list ==> ==> where "sublist [] xs" "sublist ys xs ==> sublist ys (x # xs)" "sublist ys xs ==> sublist (x # ys) (x # xs)" text ‹ Explicit check in ‹ OCaml› for correct precedence of let expressions in list expressions › definition funny_list :: "bool list" where "funny_list = [let b = True in b, False]" definition funny_list' :: "bool list" where "funny_list' = funny_list" lemma [code]:"funny_list' = [True, False]" by (simp add: funny_list_def funny_list'_def )definition check_list :: unitwhere "check_list = (if funny_list = funny_list' then () else undefined)" text ‹ Explicit check in ‹ Scala› for correct bracketing of abstractions› definition funny_funs :: "(bool ==> ==> ==> where "funny_funs fs = (λx. x ∨ True) # (λx. x ∨ False) # fs" text ‹ Explicit checks for strings etc.› definition ‹ hello = ''Hello, world!''› definition ‹ hello2 = String.explode (String.implode hello)› definition ‹ which_hello ⟷ hello ≤ hello2› end
Messung V0.5 in Prozent C=82 H=100 G=91
¤ 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.14Bemerkung:
(Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-27)
¤ *Bot Zugriff
