Re: [Hol-info] About the use of symbol | in HOL4

Hi Ada, In the first case you're trying to define a function in the HOL logic. In the second case you're defining a SML function Jeremy On 29/11/15 22:15, Ada wrote: > Hey guys, > > I am learning to use HOL. I find an interesting thing about the use of > symbol | in HOL4. > I defined an

[Hol-info] ?????? About the use of symbol | in HOL4

Thank you for your reply! if I want to use symbol | in defining a function in the HOL logic, how could I use it ? -- -- ??: "Jeremy Dawson";; : 2015??11??29??(??) 7:56 ??:

[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