Your options are not all the same. In particular, option 1 gives you a type
that can be either a reg1, or a reg2 or a reg3 or a reg4, but only one of
those. Your other options are basically the same. Options 2 and 3 are
identical (Hol_datatype is an old name for Datatype, and has a slightly
different syntax).
To manipulate record types, as in options 2 and 3, you write things like
v.reg1 (* accesses reg1 field of v *)
and
v with <| reg1 := 3; reg3 := EMPTY |> (* the record value that is like v
except with different reg1 and reg3 fields *)
There is a section in the description manual about record types (in the
Advanced Definition Principles chapter).
If you want a variant of your 4th option, you might also write
val _ = Datatype `regs = Regs num (num list) (real -> bool) (‘a # ‘b)`
Michael
From: 刘耕阳 <2015200...@mail.buct.edu.cn>
Date: Monday, 20 March 2017 at 14:40
To: "hol-info@lists.sourceforge.net" <hol-info@lists.sourceforge.net>
Subject: [Hol-info] How to define a new datatype and use it?
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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
