(* Author: Florian Haftmann, TU Muenchen *) \<open>A huge collection of equations to generate code from\<close> 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 \<open>Codegenerator_Test.drop_partial_term_of\<close> text \<open>Simple example for the predicate compiler.\<close> inductive sublist :: "'a list \ 'a list \ bool" where "sublist [] xs" "sublist ys xs \ sublist ys (x # xs)" "sublist ys xs \ sublist (x # ys) (x # xs)" text \<open>Explicit check in \<open>OCaml\<close> for correct precedence of let expressions in list expressions\<close> 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 \<open>Explicit check in \<open>Scala\<close> for correct bracketing of abstractions\<close> definition funny_funs :: "(bool \ bool) list \ (bool \ bool) list" where "funny_funs fs = (\x. x \ True) # (\x. x \ False) # fs" text \<open>Explicit checks for strings etc.\<close> definition \<open>hello = ''Hello, world!''\<close> definition \<open>hello2 = String.explode (String.implode hello)\<close> definition \<open>which_hello \<longleftrightarrow> hello \<le> hello2\<close> end quality 100%
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
