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
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
>
Call for Workshop Proposals
9th Conference on Intelligent Computer Mathematics
- CICM 2016 -
July 25-29, 2016