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

[Hol-info] First Call for Papers: Special Issue of the SCP on Automated Verification of Critical Systems

Science of Computer Programming Special Issue on Automated Verification of Critical Systems First Call for Papers Guest editors: Gudmund Grov & Andrew Ireland Submission deadline: 20 May 2016 Notification: 31 August 2016 This special issue is devoted to the 15th international workshop on

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