isabelle: src/HOL/Codegenerator_Test/RBT_Set

     1 (*  Title:      HOL/Codegenerator_Test/RBT_Set_Test.thy

     2     Author:     Ondrej Kuncar

     3 *)

     5 header {* Test of the code generator using an implementation of sets by RBT trees *}

     7 theory RBT_Set_Test

     8 imports Library "~~/src/HOL/Library/RBT_Set"

     9 begin

    11 (*

    12    The following code equations have to be deleted because they use

    13    lists to implement sets in the code generetor.

    14 *)

    16 lemma [code, code del]:

    17   "Sup_pred_inst.Sup_pred = Sup_pred_inst.Sup_pred" ..

    19 lemma [code, code del]:

    20   "Inf_pred_inst.Inf_pred = Inf_pred_inst.Inf_pred" ..

    22 lemma [code, code del]:

    23   "pred_of_set = pred_of_set" ..

    26 lemma [code, code del]:

    27   "Cardinality.card' = Cardinality.card'" ..

    29 lemma [code, code del]:

    30   "Cardinality.finite' = Cardinality.finite'" ..

    32 lemma [code, code del]:

    33   "Cardinality.subset' = Cardinality.subset'" ..

    35 lemma [code, code del]:

    36   "Cardinality.eq_set = Cardinality.eq_set" ..

    39 lemma [code, code del]:

    40   "acc = acc" ..

    42 (*

    43   If the code generation ends with an exception with the following message:

    44   '"List.set" is not a constructor, on left hand side of equation: ...',

    45   the code equation in question has to be either deleted (like many others in this file)

    46   or implemented for RBT trees.

    47 *)

    49 export_code _ checking SML OCaml? Haskell? Scala?

    51 end

author	Christian Sternagel
	Thu Aug 30 15:44:03 2012 +0900 (2012-08-30)
changeset 49093	fdc301f592c4
parent 48624	9b71daba4ec7
child 49948	744934b818c7
permissions	-rw-r--r--