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
requir
If you put exactly what you typed into HOL4, then you were using "first"
from ML rather than the one in the logic.
To do evaluation in the logic, try:
EVAL ``first [1;2;3;4] 3``
On Mon, Nov 30, 2015 at 5:29 PM, Waqar Ahmad <12phdwah...@seecs.edu.pk>
wrote:
>
>
> On Mon, Nov 30, 2015 at 12:42 P
On Mon, Nov 30, 2015 at 12:42 PM, 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 follows:
>
> - val first_def = Define`(first [] n = [] )
>/\ (first (p::pl) 0 = []
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 follows:
>
> - val first_
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 (p:
