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 <konrad.sl...@gmail.com>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 <mas.tajv...@gmail.com>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
>> hol-info@lists.sourceforge.net
>> 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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
