The following data structure is defined in HOL4.
val _ = Datatype `
my = <|
r: num;
b: num;
dis: real
|>`;
Given a mylist(:my list), if a certain condition is met, modify the
dist value in my, otherwise the dis value in my will not change. How to define
such an operation in HOL4?_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
