Here is the following code
datatype temp = C of real | F of real; fun temp_to_f
t = case t ofC x => x * (9.0 / 5.0) + 32.0 | F x
=> x;
What is the function of the function temp_to_f ? How to use this function
I recommend learning about the syntax of HOL a bit more. Also, as Michael
suggested (to you or someone else) maybe write the code up first as an SML
program and then translate to HOL. In any case, here are some nonsense
definitions that HOL allows. They should help you get further.
load
The following data types are defined in HOL4.val _ =
Datatype ` coordinate = <|
x_axis: real; y_axis: real;
z_axis: real
There seems to be some problems with the syntax. For one, the !ch ... on
the right hand side of the definition means that the rhs is boolean, which
conflicts with the record values being returned by the if-then-else.
Konrad.
On Wed, Dec 19, 2018 at 8:04 PM 幻＠未来 <849678...@qq.com> wrote:
> The
The following data types are defined in HOL4.val _ =
Datatype ` coordinate = <|
x_axis: real; y_axis: real;
z_axis: real
As written (and with a definition provided for max_distance), your script works
fine. Your error message must be for some other problem.
From your description, it sounds as if you want to use MAP to alter all ch
values in a pop (which is a chromosome list).
As it seems very computational, I’d
The following data types are defined in HOL4.
val _ = Datatype ` coordinate = <|
x_axis: real;
y_axis: real; z_axis: real
