You are close. Use MAP.
And please don’t use a mailing list to do assignments.
Michael
From: 幻＠未来 <849678...@qq.com>
Date: Tuesday, 8 January 2019 at 12:49
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 + 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?
How to write an program in SML (or Haskell, or OCaml) first,then
formalising it in HOL? Can you give a simple example?
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
