Hi,
I am a beginner of HOL4, and I want to verify the design of an algorithm.
The first step of my work is to define the basic type of the
algorithm.Through information research, I find 4 methods:
1 Datatype `test = reg1 num | reg2 (num list) | reg3 (real -> bool) | reg4
'a#'b`;
2 Datatype `test = <|reg1: num; reg2: num list; reg3: (real -> bool); reg4:
'a#'b|>`;
3 val _= Hol_datatype `
test = <|
reg1 : num;
reg2 : num list;
reg3 : real -> bool;
reg4 : 'a # 'b
|>`;
4 type_abbrev("test", ``: num#(num list)#(real -> bool)#('a#'b)``);
I don't know what are they differences, and how can I use it(e.g.If I want to
use reg3 in test, how can I operating it?).
I've been confused for a week, and I queryed kananaskis-10-description and
kananaskis-10-reference,but they are not detailed.Does anyone can help me?
Thanks!------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
