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 + 1000 |>)
else (ch with <| distance := ch.distance |>)`;
Given a pop(:chromosome list),ch is an element in pop. For any ch, if a
certain condition is met, the value of distance in ch is increased by 1000 on
the basis of the original value, otherwise it is unchanged. How to achieve this?_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
