Re: [Hol-info] Element assignment in structures

HOL is not an imperative language, so you can’t “assign” fields of a record. However, you can write things like My_record with <| b := 3; rx := x’; distance := 10.6 |> to denote a chromosome value that is the same as My_record except that fields b, rx and distance have different values.

[Hol-info] Element assignment in structures

Hello! I defined the following data structure in HOL4. Datatype ` chromosome = <| r: num; b: num; distance: real;