[isabelle] Isabelle 2016-RC2: warnings in generated code for GCD and LCM



Dear all,

I just noticed, that there are overlapping patterns in the generated code for LCM and GCD, if one loads Code_Target_Int.
It seems that the original code-equations have not been deactivated. So, one gets warnings when compiling the generated
Haskell-code.

Best regards,
RenÃ

theory Scratch
imports 
  "~~/src/HOL/Library/Code_Target_Int"
begin

definition  "f (x :: int) = gcd 5 (lcm x 7)"

export_code f in Haskell

(* 
gcd_int :: Arith.Int -> Arith.Int -> Arith.Int;
gcd_int (Arith.Int_of_integer x) (Arith.Int_of_integer y) = Arith.Int_of_integer (Prelude.gcd x y);
gcd_int k l = Arith.abs_int
    (if Arith.equal_int l Arith.zero_int then k
      else gcd_int l (Arith.mod_int (Arith.abs_int k) (Arith.abs_int l)));

lcm_int :: Arith.Int -> Arith.Int -> Arith.Int;
lcm_int (Arith.Int_of_integer x) (Arith.Int_of_integer y) =
  Arith.Int_of_integer (lcm_integer x y);
lcm_int a b =
  Arith.divide_int (Arith.times_int (Arith.abs_int a) (Arith.abs_int b))
    (gcd_int a b);

*)



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.