Dear all,
I am using Hol-light on Ubuntu 14.04. I am facing theory loading conflict.
I am loading only two theories in alternative sequences but in both cases I
am having problems. The theories are *Multivariate/cauchy.ml
<http://cauchy.ml>* and *Library/poly.ml <http://poly.ml>*.
In the first case, when I load cauchy theory first, it ends up with the
following error:
-------------------------------------------------------------------------------
File "/home/user/hol-light-workbench/hol-light/Multivariate/cauchy.ml",
line 12911, characters 35-58:
Error: Unbound value REAL_LOG_CONVEX_ON_SING
Error in included file
/home/user/hol-light-workbench/hol-light/Multivariate/cauchy.ml
val it : unit = ()
-------------------------------------------------------------------------------
After this, I load the poly theory which also ends up with the following
error:
-------------------------------------------------------------------------------
File "/home/user/hol-light-workbench/hol-light/Library/poly.ml", line 173,
characters 51-61:
Error: Unbound value DIFF_CONST
Error in included file /home/user/hol-light-workbench/hol-light/Library/
poly.ml
val it : unit = ()
-------------------------------------------------------------------------------
In this sequence of loading theories, it does not recognize the theorems
when entered in shell.
e.g.
*REAL_CONTINUOUS_ATREAL_WITHINREALError: Unbound value
REAL_CONTINUOUS_ATREAL_WITHINREAL*
Where as, in the second case, when I load poly theory first, it ends up
fine. Next, when I load the cauchy theory, it ends up with the following
error:
---------------------------------------------------------------------------------
Error in included file
/home/user/hol-light-workbench/hol-light/Multivariate/realanalysis.ml
- : unit = ()
File "/home/user/hol-light-workbench/hol-light/Multivariate/moretop.ml",
line 23, characters 45-64:
Error: Unbound value OPEN_CONTAINS_CBALL
Error in included file
/home/user/hol-light-workbench/hol-light/Multivariate/moretop.ml
- : unit = ()
- : unit = ()
- : unit = ()
Exception:
Failure
"typechecking error (initial type assignment): f cannot have type
real->(_->bool)->bool and real->real simultaneously".
Error in included file
/home/user/hol-light-workbench/hol-light/Multivariate/cauchy.ml
val it : unit = ()
------------------------------------------------------------------------------
In this case, when I write a goal involving exponential (exp) function, it
gives error* Exception: Noparse* else it works fine.
If I try only cauchy theory without loading poly theory, it results no
error when using exp function, which, to me, shows that *Noparse* error is
not due to brackets.
Thanks in advance.
------------------------------------------------------------------------------
Dive into the World of Parallel Programming. The Go Parallel Website,
sponsored by Intel and developed in partnership with Slashdot Media, is your
hub for all things parallel software development, from weekly thought
leadership blogs to news, videos, case studies, tutorials and more. Take a
look and join the conversation now. http://goparallel.sourceforge.net/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
