Thank you for your answer. I made the following attempt in HOL4.
open realLib;
val _ = Datatype `
coordinate = <|
x_axis: real;
y_axis: real;
z_axis: real
|> `;
val _ = Datatype `
chromosome = <|
r: num;
b: num;
distance: real;
rx: coordinate;
path: coordinate list;
bx: coordinate
|> `;
``ch with <| b := 3; distance := 10.6 |> ``;
Can I print out the values of b and distance in ch? How can I
print?
In addition, I made the following definition in HOL4
val robot_judge_def = Define `
robot_judge pop = !ch RB robot. is_robot_object RB /\ MEM
ch pop /\
MEM robot RB.robotpoint /\ robot.r <
ch.r ==>
if MEM robot.point ch.path then (ch with
<| distance := ch.distance + 1000 |>)
else (ch with <| distance := ch.distance
|>) `;
First of all, when certain conditions are met, I want to increase the
distance value in ch by 1000 based on the original value. Is Term ``ch with <|
distance := ch.distance + 1000 |>`` feasible?
In addition, this definition is wrong. Is there any way to do what I
want to do?
QIN_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
