coq - 如何找到自然数列表的最小元素

Question

如何找到列表中的最小元素？Coq 库中是否有任何内置函数可以使用？我有搜索列表分钟但什么也没找到。

标签： coq

Answer 1

From Coq Require Import Nat.

Fixpoint min_elem xs :=
  match xs with
  | nil => 0
  | x :: nil => x
  | x :: xs' => Nat.min x (min_elem xs')
  end
.