Email Gateway (Aug 19 2022 at 14:49): Email Gateway (Aug 19 2022 at 14:49):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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 *)
Last updated: Apr 25 2024 at 08:20 UTC