findMax

write a function that, given a List of integers, finds its maximum

Function Signature

import Init.Data.List

def findMax (xs : List Int) : Option Int 

Theorem Signature

theorem findMax_correct(x: Int) (xs : List Int):
  ∃ max∈ (x::xs),
    And (findMax (x::xs) = some max) (∀ y ∈ (x::xs) , y ≤ max) 

Additional Theorem Signature

theorem findMax_base : findMax [] = none

View All Submissions

Please log in or register to submit a solution for this challenge.