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