I am new to Idris, so forgive me if this a dumb question.
When doing Exercise 5 on page 101 of the TypeDD book, my solution (which is the same as the suggested solution in this repository) exhibits the following behavior when I launch idris ex_4_1.idr:
Type checking ./ex_4_1.idr
*ex_4_1> maxMaybe Nothing Nothing
Can't find implementation for Ord a
According to the definition of maxMaybe (included below for reference), it seems the answer should be Nothing. Is this an error? Do I not have Idris set up correctly?
maxMaybe : Ord a => Maybe a -> Maybe a -> Maybe a
maxMaybe Nothing Nothing = Nothing
maxMaybe Nothing (Just y) = Just y
maxMaybe (Just x) Nothing = Just x
maxMaybe (Just x) (Just y) = Just (max x y)
I am new to Idris, so forgive me if this a dumb question.
When doing Exercise 5 on page 101 of the TypeDD book, my solution (which is the same as the suggested solution in this repository) exhibits the following behavior when I launch
idris ex_4_1.idr:According to the definition of
maxMaybe(included below for reference), it seems the answer should beNothing. Is this an error? Do I not have Idris set up correctly?