Hi Ada,
You need to search for suitable theorems.
In this case
> apropos ``TAKE 0`` ;
<>
val it =
[(("list", "TAKE_0"), (|- TAKE 0 l = [], Thm)),
so from the initial goal
e (STRIP_ASSUME_TAC listTheory.LENGTH_EQ_NUM_compute);
e (ASM_REWRITE_TAC [listTheory.TAKE_0]) ;
This should work bu
fs[LENGTH_NIL,TAKE_def]
On 15 December 2015 at 14:27, Ada wrote:
> Hey guys,
>
> I am learning to use HOL4. There is a function named "TAKE" in HOL4,
> which can get the first n elements in a list.
> When I was proving one property of TAKE, I find an interesting thing. As
> follows:
> - g`!p:bo
Hey guys,
I am learning to use HOL4. There is a function named "TAKE" in HOL4, which can
get the first n elements in a list.
When I was proving one property of TAKE, I find an interesting thing. As
follows:
- g`!p:bool list n:num. (LENGTH p = 0) ==> (TAKE 0 p = p) `;
- e (REPEAT STRIP_TAC);
Call for Workshop Proposals
9th Conference on Intelligent Computer Mathematics
- CICM 2016 -
July 25-29, 2016
U
ITP 2016: CALL FOR PAPERS
The Seventh International Conference on Interactive Theorem Proving
22 to 26 August 2016, Nancy, France
http://itp2016.inria.fr/
The ITP conference series is concerned with all topics related to interactive
theorem proving, ranging from theoretical foundations to implem
