Hi, I have a situation like this that makes removing a defined term desirable. I first define a function:
val FOO_def = Define `FOO bsp ksp = ...` and later its parameter val bsp_def = Define `bsp = ...` I define bsp_def, because the right hand side of bsp definition is very long for which I'd like to use a short name for it (in this case, it's simply "bsp"), so I can easily see the function application. However, after I experiment with the definition of FOO and change it, I can't run the FOO definition again. HOL complaints occur. Then I have to change the parameter names in FOO to others such as bsp1, ksp1 etc. in the FOO definition. This is error-prone and often becomes inefficient. Is there a way to remove the definition of bsp so that I don't have to change the names of parameters of FOO? I know avoiding defining bsp can solve this problem, but when I experiment many definitions, it's very difficult to not define a constant that happens to be a function parameter. Thanks. Lu ------------------------------------------------------------------------------ The ultimate all-in-one performance toolkit: Intel(R) Parallel Studio XE: Pinpoint memory and threading errors before they happen. Find and fix more than 250 security defects in the development cycle. Locate bottlenecks in serial and parallel code that limit performance. http://p.sf.net/sfu/intel-dev2devfeb _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
