[isabelle] Code_Abstract_Nat raises exception for a variable with name g



I'd like to report that the simproc in Code_Abstract_Nat raises an exception about a variable with name g having different types during the preprocessing phase of the code generator if there is a 0/Suc-group of code equations that involve a variable g whose type does not coincide with the return type of the function. The exception disappears if I rename the variable g in the code equations to something else.

Below is a minimal example for Isabelle2013-2 and a recent development version (697e0fad9337).

Andreas


theory Scratch imports Main "~~/src/HOL/Library/Code_Abstract_Nat" begin

primrec foo :: "int => nat => bool" where
  "foo g 0 = False"
| "foo g (Suc n) = g True"

declare [[show_types]]

code_thms foo

(* exception TYPE raised (line 114 of "envir.ML"):
   Variable has two distinct types
   ?g ∷ bool ⇒ bool
   ?g ∷ bool *)




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