実務

Coqで同値関係

最近仕事でlistの要素を仲間分けしてリストのリストを返す 次のような関数をOCamlで定義した。 let rec classify rel l = match l with | [] -> [] | x::xs -> let (ys,zs) = List.partition (fun y -> rel x y) xs in (x, ys) :: classify rel zs この関数…