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 幻＠未来 <849678...@qq.com> 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 > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info >
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
