Lean4 で選択ソートを実装してみました．
部分関数として
import Mathlib.Tactic
universe uu
open List
variable {α : Type uu} [Min α] [DecidableEq α]
partial def SelectionSort : List α → List α
| [] => []
| x :: xs =>
let min := minimum? (x :: xs)
match min with
| none => []
| some μ =>
μ :: SelectionSort ((x :: xs).erase μ)
与えられた配列の最小値 μ を取り，μ を先頭に持ってくるのと同時に，μ を未ソート領域から削除します．これを帰納的に繰り返すというコードです．
minimum? というのはリストの最小値をとる関数ですが，返り値が Option になっています．空のリストの場合は none を返します．
そしてこれが重要なのですが，partial と書かれているのは，この関数が有限回で停止することが証明されていないことを意味します．停止性を証明するには，引数に渡しているリストのサイズが，再帰呼び出しのたびに減少することを証明すれば十分です．
この「有限回で停止することを示すか，partial とマークしないとエラーになる」という定理証明支援系としての性質は面倒でもありますが，ほかの言語，たとえば Haskell だと実行するまで気が付かなくて無限ループになってクラッシュしてしまったりするわけで，それが未然に防げると考えると良いかもしれません．
停止性
次のようなコードで，停止性が保証された関数として定義できます：
def SelectionSort (l : List α) : List α :=
if 0 < l.length then
let min := minimum? l
match min with
| none => []
| some μ =>
if mem : μ ∈ l then
have : l.length > (l.erase μ).length :=
calc l.length
_ = (l.erase μ).length + 1 := by rw [← length_erase_add_one mem]
_ > (l.erase μ).length := by linarith
μ :: SelectionSort (l.erase μ)
else []
else []
termination_by SelectionSort l => l.length
if mem : μ ∈ l then というところに注目してください．単なるパターンマッチだと，パターン分岐による変数の情報にアクセスできないので，if 式の中で分岐条件に名前をつけています．
l.erase というのはリストから要素を高々一つ削除するような関数ですが，erase がまるでリストオブジェクトのメソッドであるかのようにドット記法でアクセスできるのがおもしろいですね．
補足
ところで，上記コードをもう一度見てください．
μ はリスト l の最小値として定義されているので，if mem : μ ∈ l then という条件分岐がなぜ必要なのか疑問に思いませんか？
実はここで型 α に対して，線形順序という仮定はありませんので，互いに比較不能な元がリストに入っている可能性があります．そのために分岐が必要になっています．
型 α に線形順序を仮定すると，ここの if 式はいらなくなります．
import Mathlib.Tactic
universe uu
open List
variable {α : Type uu}
def SelectionSort [LinearOrder α] (l : List α) : List α :=
if hl : 0 < l.length then
let μ : α := minimum_of_length_pos hl
have mem : μ ∈ l := minimum_mem (by simp)
have : l.length > (l.erase μ).length :=
calc l.length
_ = (l.erase μ).length + 1 := by rw [← length_erase_add_one mem]
_ > (l.erase μ).length := by linarith
μ :: SelectionSort (l.erase μ)
else []
termination_by SelectionSort l => l.length
