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
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 Datatyp
ABSTRACT REGISTRATION DEADLINE EXTENDED TO April 26 ***
PAPER SUBMISSION DEADLINE EXTENDED TO May 2 ***
ICLP 2017 Call for Papers
-
The 33rd International Conference on Logic Programming (ICLP 2017)
will take place in Melb
Dear List Members,
1. An earlier statement of mine in the HOL and Isabelle mailing lists on R0 has
to be corrected. The claim that "Unlike all other existing proof assistants or
proof checkers, it is a Hilbert-style system", has to be relativized, since,
depending on how strictly a Hilbert-styl
