You can’t access those theorems directly at the ML level in the session where
they’re defined (unfortunately). They do appear under the right names in
descendant theories. Within the same script file, you have to manually bind it
at the ML level:
val coordinate_component_equality = theorem “coordinate_component_equality”
Michael
From: Liu Gengyang <2015200...@mail.buct.edu.cn>
Date: Friday, 15 September 2017 at 12:00
To: hol4_QA <hol-info@lists.sourceforge.net>
Subject: [Hol-info] A small question about Datatype.
Hi,
I have a small question about Datatype. I define a type coordinate as follow:
Datatype `coordinate = <|
x_axis: real;
y_axis: real;
z_axis: real |>`;
it derived and stored some relevant theorems, like
coordinate_component_equality, now I want to use this theorem, I tried to call
it by coordinate_component_equality or
scratchTheory.coordinate_component_equality, but failed.I queried HOL handbooks
and still don't know how to call it, could anyone tell me how to call it?
Regards,
Liu
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
