[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).
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"
(* 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