Thiemann, Rene

2016-09-30 07:54:22 UTC

Dear list,

we just stumbled upon the translation of pattern matching of natural numbers for code-generation in the presence of target-language integers.

theory Test

imports

Main

"~~/src/HOL/Library/Code_Target_Numeral"

begin

fun foo :: "nat ⇒ bool" where

"foo (Suc 0) = True"

export_code foo in Haskell

(* "Nat.Suc" is not a constructor, on left hand side of equation, in theorem:

foo (Suc zero_nat_inst.zero_nat) ≡ True *)

end

Of course, it is easy to work around by providing suitable code-equations manually, but perhaps this can be fixed in the future.

The problem occurs in both Isabelle 2016 and in the development version d4b89572ae71.

Cheers,

Akihisa and René

we just stumbled upon the translation of pattern matching of natural numbers for code-generation in the presence of target-language integers.

theory Test

imports

Main

"~~/src/HOL/Library/Code_Target_Numeral"

begin

fun foo :: "nat ⇒ bool" where

"foo (Suc 0) = True"

export_code foo in Haskell

(* "Nat.Suc" is not a constructor, on left hand side of equation, in theorem:

foo (Suc zero_nat_inst.zero_nat) ≡ True *)

end

Of course, it is easy to work around by providing suitable code-equations manually, but perhaps this can be fixed in the future.

The problem occurs in both Isabelle 2016 and in the development version d4b89572ae71.

Cheers,

Akihisa and René