The following data types are defined in HOL4. 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
|> `;
val ch = ``ch: chromosome``;
val pop = ``pop: chromosome list``;
Given a pop(:chromosome list), I want to achieve a goal : If if-condition
is met, the distance value of the ch in the pop is assigned to other values,
otherwise the distance value of ch is unchanged. How to solve this problem? How
to define such an operation?_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
