Thank you for your answer. I made the following attempt in HOL4.
open realLib;
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``;
ch with <| b := 3; rx := x'; distance := 10.6 |>;
But gave such an error :
> poly: : error: ; expected but with was found
Static Errors
> poly: : error: Value or constructor (<|) has not been declared
Found near <| b := 3
Static Errors
> poly: : error: Value or constructor (rx) has not been declared
Found near rx := x'
poly: : error: Value or constructor (x') has not been declared
Found near rx := x'
Static Errors
> poly: : error: <identifier> expected but ; was found
Static Errors
How can this be solved? Thank you for your patience.
Qin_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
