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.
Michael
From: 幻＠未来 <849678...@qq.com>
Date: Tuesday, 18 December 2018 at 13:57
To: hol-info <hol-info@lists.sourceforge.net>
Subject: [Hol-info] Element assignment in structures
Hello!
I defined the following data structure in HOL4.
Datatype `
chromosome = <|
r: num;
b: num;
distance: real;
rx: coordinate;
path: coordinate list;
bx: coordinate
|>`;
So, how do you assign values and modify values to elements in a structure?
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
