2014-07-12 ■ coqのワイルドカードって、データしかあかんのか? Fixpoint bin_len (b : bin) : nat := match b with | Q => O | T b' => S (bin_len b') | F b' => S (bin_len b') end.を Fixpoint bin_len (b : bin) : nat := match b with | Q => O | _ b' => S (bin_len b') end. と書くことは出来ないのか?