findMin

write a function that, given a List of integers, finds the minimum

Function Signature

import Init.Data.List

def findMin (xs : List Int) : Option Int 

Theorem Signature

theorem findMin_correct(x: Int) (xs : List Int):
  ∃ min∈ (x::xs),
    And (findMin (x::xs) = some min) (∀ y ∈ (x::xs) , y >= min) 

Additional Theorem Signature

theorem findMin_base : findMin [] = none

View All Submissions

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