Re: [Hol-info] [SPAM] some questions about the proving process in HOL4

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

Re: [Hol-info] [SPAM] some questions about the proving process in HOL4

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 >