Re: [Hol-info] some questions about the use of HD and TL in listTheory

Hi Ada, when you enter first ([0,1,0,1,0],3); this refers to the SML function first whose type is given by first ; val it = fn: ('a -> bool) -> 'a list -> 'a What you want is the HOL term ``first ([0,1,0,1,0],3)`` which will also give you a type error, since your definition of first

Re: [Hol-info] some questions about the use of HD and TL in listTheory

HOL syntax for lists uses semicolons (;) to separate list elements, not commas (,). On 30 November 2015 at 18:42, Ada wrote: > 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

[Hol-info] some questions about the use of HD and TL in listTheory

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::pl) 0 = [] ) /\ (first (p::pl) n = HD