Thank you
So helpful, this is my function now,( which is working properly):
val Max_List = Define `( Max_List []= NONE)
/\ ( Max_List (h::l) = let max= Max_List l in
( if h >THE( max) then SOME h
else if h = THE( max) then NONE
else Max_List l ))`
On Fri, Apr 25, 2014 at 4:02 AM, Konrad Slind <[email protected]>wrote:
> The code has a mistake which results in
>
> !l. Max_List l = NONE
>
> being provable which is probably undesirable. This can
> be repaired by adding a clause
>
> (Max_List [x] = SOME x)
>
> to the definition/ Also, you might consider changing it to
> use >= rather than >.
>
> Konrad.
>
>
>
> On Thu, Apr 24, 2014 at 12:07 PM, Konrad Slind <[email protected]>wrote:
>
>> Hi,
>>
>> Problem is that the max computed on the tail of the list
>>
>> let max = Max_List l
>>
>> is an element of an option type, so has the form of NONE or SOME m.
>> However, you are directly comparing max with a number. So the type
>> system is angry at you!
>>
>> Try this instead:
>>
>> val Max_List =
>> Define
>> `(Max_List [] = NONE) /\
>> (Max_List (h::t) =
>> case Max_List t
>> of NONE => NONE
>> | SOME max => if max > h then SOME max else
>> if h > max then SOME h else NONE)`;
>>
>>
>>
>>
>>
>> On Thu, Apr 24, 2014 at 4:51 AM, masoume tajvidi
>> <[email protected]>wrote:
>>
>>> Hi,
>>> My function for finding the max number of a list is as follows:
>>> val Max_List = Define ( Max_List []= NONE)
>>>
>>> /\ ( Max_List (h::l) = let max= Max_List l in
>>>
>>> ( if h > max then SOME h else if h = max then NONE
>>>
>>> (else( Max_List l)))
>>>
>>> I do not know whats wrong with this?
>>> Can anybody help please?
>>> when I use 0 instead of zero it works properly.
>>>
>>> Thanks a lot
>>>
>>>
>>> ------------------------------------------------------------------------------
>>> Start Your Social Network Today - Download eXo Platform
>>> Build your Enterprise Intranet with eXo Platform Software
>>> Java Based Open Source Intranet - Social, Extensible, Cloud Ready
>>> Get Started Now And Turn Your Intranet Into A Collaboration Platform
>>> http://p.sf.net/sfu/ExoPlatform
>>> _______________________________________________
>>> hol-info mailing list
>>> [email protected]
>>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>>
>>>
>>
>
------------------------------------------------------------------------------
Start Your Social Network Today - Download eXo Platform
Build your Enterprise Intranet with eXo Platform Software
Java Based Open Source Intranet - Social, Extensible, Cloud Ready
Get Started Now And Turn Your Intranet Into A Collaboration Platform
http://p.sf.net/sfu/ExoPlatform
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
