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 MEM ch pop then (ch with <| distance :=
ch.distance + max_distance pop |>)
else (ch with <| distance := ch.distance |>)`;
val get1_def = Define `
get1 pop = !ch. if MEM ch pop then (ch.distance = ch.distance +
max_distance pop)
else ch.distance = ch.distance`;
The definition of get_def is successful, but the definition of get1_def is
unsuccessful. Defining get1_def will report an error:
Exception raised at Preterm.type-analysis:
roughly between line 878, character 19 and line 879, character 58:
Type inference failure: unable to infer a type for the application of
($! :(?? -> bool) -> bool) :(?? -> bool) -> bool
on line 878, characters 14-17
to
??(ch :chromosome).
if MEM ch (pop :chromosome list) then
ch with distance := ch.distance + max_distance pop
else ch with distance := ch.distance
roughly between line 878, character 19 and line 879, character 58
which has type
:chromosome -> chromosome
unification failure message: Attempt to unify different type operators:
min$bool and scratch$chromosome
What I want to do is to give a pop(:chromosome list), for any
ch(:chromosome) in the pop , if some conditions are met, then the distance
value in ch is modified. How to solve this problem?_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
