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
