Hi Ada, It's just
val fir_def = Define`(fir [] n = [] ) /\ (fir p 0 = [])`; ie what's between the backquotes looks just like a statement in the HOL logic Cheers, Jeremy On 29/11/15 23:08, Ada wrote:> 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";<jeremy.daw...@anu.edu.au>; > *????????:* 2015??11??29??(??????) ????7:56 > *??????:* "????"<ada.k...@qq.com>; > "hol-info"<hol-info@lists.sourceforge.net>; > *????:* 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 function named fir, as follows: > > - val fir_def = Define` > > (fir [] n = [] ) | > > (fir p 0 = [])`; > > But failed , it responsed that: > > Don't expect to find a | in this position after a <beginning of input> > > at line 5, character 22 and in compiler-generated text. > > Exception raised at Absyn.Absyn: > > in compiler-generated text: > > Don't expect to find a | in this position after a <beginning of input> > > at line 5, character 22 and in compiler-generated text. > > ! Uncaught exception: > > ! HOL_ERR > > Then, I tried again , as follows: > > - fun fir ([] , n) = [] > > | fir (p ,0 )= [] ; > > It succeeded. > > Now, I have two questions: > > 1??Why can't the symbol | be used in "Define"? > > 2??What are the differences between "Define" and "fun"? > > Thanks! --Wish. > > > > > > > ------------------------------------------------------------------------------ > > > > > > > > _______________________________________________ > > hol-info mailing list > > hol-info@lists.sourceforge.net > > https://lists.sourceforge.net/lists/listinfo/hol-info > > ------------------------------------------------------------------------------ _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
