Dear Marco,
Many thanks for your response. When I first load the file Multivariate/
make_complex.ml, and then the Library/poly.ml theory, it ends up with the
same error as mentioned in the last email.
I tried the alternate sequence of these two theories, the problem still
persists.
There is a definition named *poly_exp* in theory Library/poly.ml which is:
*|- p exp 0 = [&1] /\ p exp SUC n = p ** p exp n*
it takes a real list and a num and return a real list.
When I want to use the simple exponential (exp) function which is:
*|- !x. (exp) x = Re (cexp (Cx x))*
It gives me error mentioned in last email. So, it looks like a conflict
between these two exponentials.
On Fri, Feb 13, 2015 at 7:18 PM, Marco Maggesi <[email protected]>
wrote:
> Dear Adnan,
>
> the expected way to use Multivariate/cauchy.ml is by loading the file
> Multivariate/make_complex.ml which in turn loads all the dependencies in
> the appropriate order (including cauchy.ml).
>
> You also must be warned that loading complex analysis may take a while
> (say 30 minutes, but obviously it depends on your setting).
>
> Hope it helps,
> Marco
>
>
> 2015-02-13 9:32 GMT+01:00 Adnan Rashid <[email protected]>:
>
>> 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
>>
>>
>
--
Adnan Rashid
Ph.D Student,
School of Electrical Engineering and Computer Science (SEECS),
NUST, Sector H-12, Islamabad, Pakistan.
Mobile: +92-302-5156727
------------------------------------------------------------------------------
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
