Coq does not support variable shadowing, so the following SML code:
val x = 1
val x = 2
would not be correctly translated.
A solution to this problem involves keeping track of the scope a variable is declared and used, and a mapping from (variable, scope) -> new_name, where new_name is the name of the variable to be used in Coq.
Coq does not support variable shadowing, so the following SML code:
would not be correctly translated.
A solution to this problem involves keeping track of the scope a variable is declared and used, and a mapping from (variable, scope) -> new_name, where new_name is the name of the variable to be used in Coq.