Re: [Hol-developers] More explicit substitutions

[Ken F. L. <kf...@it...>]

Sorry to follow-up on my own mail.  But on my way to work, I just
thought of an obvious way to remove the Dummy structure from the
structure namespace, use local:

---
structure RawType = struct 
datatype t = Var of string | Tyop of string * t list
end;

structure RawTerm = struct 
datatype term = Con of string | App of term * term 
fun f (Con s) = RawType.Var s
  | f (App(t1,t2)) = RawType.Tyop("app", [f t1, f t2])
end;
          


local 
    structure Dummy :> sig structure Type : sig type t end
                           structure Term : 
                                     sig 
                                         type term 
                                         val f : term -> Type.t
                                         val Con : string -> term
                                         val App : term * term -> term
                                     end 
                       end =
    struct
    structure Type = RawType          
    structure Term = RawTerm
    end
in
structure Type = Dummy.Type          
structure Term = Dummy.Term
end
---


--Ken