Put them inside double backquotes: ``ch with ...``, that whole thing is a term in HOL.
> Il giorno 18 dic 2018, alle ore 08:04, 幻＠未来 <849678...@qq.com> ha scritto: > > 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 _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
