Transformation apply failed: unbound variable
The application of test_bad with 0
to the goal in the following example raises the exception “Please report: Transformation apply test_bad with 0 failed: Unbound variable: y: int”.
Making the variable y
local to z
as in test_good
is a workaround.
module Test
inductive test int =
| test_bad: forall x.
let y = x in
let z = y in
test z
| test_good: forall x.
let z =
let y = x in
y
in
test z
goal g: test 0
end