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: 幻＠未来 <849678...@qq.com>
Date: Tuesday, 8 January 2019 at 12:01
To: hol-info <hol-info@lists.sourceforge.net>
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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
