やりたいこと

Coq

Require Import List.
Require Import Arith.

Fixpoint binarize (l : list nat)(th : nat) : list nat :=
  match l with
  | nil => nil
  | x::xs => if leb th x then 255 :: (binarize xs th) else 0 :: (binarize xs th)
  end.

• 関数を適用する前と後で配列の要素数に変化がない
• 関数適用後の配列には値が0か255の2種類しかない