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``;
val get_def = Define `
get pop = !ch if (Certain condition) then (ch with <| distance :=
ch.distance + max_distance pop |>)
else (ch with <| distance := ch.distance |>)`;
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?_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
