Coqタクティクス総選挙
投票期間： 2012/04/27 00:52 ～ 2012/04/30 00:52 (終了)
destruct A as [A|[A|(A,A1)]]; destruct B; destruct C; try (contradiction || (exfalso;omega)); destruct H; [trivial|omega]. 的なソレ
17| 1 | inversion |
  |
|---|---|---|
| 1 | reflexivity |
  |
| 3 | admit |
 |
| 3 | apply |
 |
| 3 | assert |
 |
| 3 | auto |
 |
| 3 | contradiction |
 |
| 3 | destruct |
 |
| 3 | discriminate |
 |
| 3 | exact |
 |
| 3 | functional induction |
 |
| 3 | pose proof |
 |
| 3 | refine |
 |
| 3 | rewrite |
 |
| 3 | ;[|] |
 |
| case | ||
| change | ||
| clear | ||
| cofix | ||
| compute | ||
| congruence | ||
| contradict | ||
| cut | ||
| decompose | ||
| do | ||
| eval | ||
| exfalso | ||
| exists | ||
| f_equal | ||
| fail | ||
| field | ||
| fix | ||
| fold | ||
| fourier | ||
| fun | ||
| idtac | ||
| induction | ||
| injection | ||
| intros | ||
| intuition | ||
| lazymatch | ||
| match | ||
| move | ||
| nsatz | ||
| omega | ||
| psatz | ||
| red | ||
| remember | ||
| rename | ||
| replace | ||
| repeat | ||
| revert | ||
| right | ||
| ring | ||
| setoid_replace | ||
| simpl | ||
| specialize | ||
| split | ||
| stepl | ||
| stepr | ||
| symmetry | ||
| tauto | ||
| transitivity | ||
| trivial | ||
| try | ||
| unfold | ||
| vm_compute | ||
| || | ||
| ; |
ジャンル：
その他