<div dir="ltr"><div><div>Hi all,<br><br></div>I've been translating the namespace type on env-refactor, but I ran into a name clash problem:<br><br></div>The following term gets anti-quoted out for tDefine:<br><div><br>[ANTIQUOTE<br>      ``(NAMESPACE_NAMESPACE_TYPE :<br>    (ν -> v -> bool) -><br>    (ξ -> v -> bool) -><br>    (φ -> v -> bool) -> (ν, ξ, φ) namespace -> v -> bool)<br>    (m :ν -> v -> bool) (n :ξ -> v -> bool) <b>(v :φ -> v -> bool)</b><br>    (Bind (x_2 :(ξ, φ) alist) (x_1 :(ν, (ν, ξ, φ) namespace) alist))<br>    <b>(v :v)</b> ⇔<br>  ∃(v1_1 :v) (v1_2 :v).<br>    v =<br>    Conv<br>      (SOME<br>         ("Bind",<br>          TypeId (Short "namespace_namespace" :(tvarN, tvarN) id)))<br>      [v1_1; v1_2] ∧<br>    CONTAINER<br>      (LIST_TYPE :(ξ # φ -> v -> bool) -> (ξ, φ) alist -> v -> bool)<br>      (λ(x :ξ # φ) (v' :v).<br>         if MEM x x_2 then<br>           CONTAINER<br>             (PAIR_TYPE :(ξ -> v -> bool) -><br>                         (φ -> v -> bool) -> ξ # φ -> v -> bool)<br>             (λ(y :ξ) (v :v). if y = FST x then n y v else (ARB :bool))<br>             (λ(y :φ) (v' :v).<br>                if y = SND x then v y v' else (ARB :bool)) x v'<br>         else (ARB :bool)) x_2 v1_1 ∧<br>    CONTAINER<br>      (LIST_TYPE :(ν # (ν, ξ, φ) namespace -> v -> bool) -><br>                  (ν, (ν, ξ, φ) namespace) alist -> v -> bool)<br>      (λ(x :ν # (ν, ξ, φ) namespace) (v' :v).<br>         if MEM x x_1 then<br>           CONTAINER<br>             (PAIR_TYPE :(ν -> v -> bool) -><br>                         ((ν, ξ, φ) namespace -> v -> bool) -><br>                         ν # (ν, ξ, φ) namespace -> v -> bool)<br>             (λ(y :ν) (v :v). if y = FST x then m y v else (ARB :bool))<br>             (λ(y :(ν, ξ, φ) namespace) (v' :v).<br>                if y = SND x then NAMESPACE_NAMESPACE_TYPE m n v y v'<br>                else (ARB :bool)) x v'<br>         else (ARB :bool)) x_1 v1_2``]<br><br></div><div>However, it has two instances of v at different types (in bold), and it doesn't parse back in as a term (probably HOL decided to use the later instance for type checking?).<br><br></div><div>The problem seems to be that the namespace is defined with 'v as one of its type variables and "v" is used all over the translator.<br><br></div><div>There are a couple of quickfixes possible, and I was wondering which one seems better:<br><br></div><div>1) Make namespace use some other type variable<br><br></div><div>2) Add unlikely suffixes to autogenerated variable names from type variables<br></div><div><br>3) Make translator check for presence of "v" when picking variable names<br><br></div></div>