Your problem statement doesn’t make sense. Why do you say “*the* ch in the pop”? Surely a pop may contain multiple ch values.
As I said before, it seems as if you should try to write your program in SML (or Haskell, or OCaml) first. Then you might think about formalising it in HOL. If you want to adjust all the values in a list, look at the map function (called MAP in HOL). Michael From: 幻＠未来 <[email protected]> Date: Tuesday, 8 January 2019 at 12:01 To: hol-info <[email protected]> Subject: [Hol-info] assignment 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 [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
