There seems to be some problems with the syntax. For one, the !ch ... on the right hand side of the definition means that the rhs is boolean, which conflicts with the record values being returned by the if-then-else.
Konrad. On Wed, Dec 19, 2018 at 8:04 PM 幻＠未来 <[email protected]> wrote: > 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 >
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
