Hi Ada,
You have defined the function "first" on an arbitrary type list. It can be
specified for any type of list in the proof goal. For instance, you can
verify the following property on the "bool list":
g `!(L:bool list) n. n <= LENGTH L ==> (LENGTH (first L n) = n)`;
On Mon, Dec 7, 2015 at
The 8th NASA Formal Methods Symposium
-
http://crisys.cs.umn.edu/nfm2016
June 07 - June 09 2016
McNamara Alumni Center
University of Minnesota
200 Oak Street S.E., Minneapolis, MN 55455
Theme of the Symposium
--
The widespread use and in
Hey guys,
I am learning to use HOL4. I defined a function named "first" in HOL4. This
function can get the first n elements in a list. As follows:
- val first_def = Define`(first [] n = [] )
/\ (first p 0 = [] )
/\ (first p n = HD p :: first (TL
