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
