All Tasks

# Name Publish time Difficulty Compiler Source code policy
40 Binary search 2019/12/08 20:00:00 3 Coq 8.9.1 Public
39 Boolean-hole principle revisited 2019/12/08 20:00:00 2 Coq 8.9.1 Public
38 Midpoint 2019/12/08 20:00:00 1 Coq 8.9.1 Public
37 Zero test 2019/12/08 20:00:00 1 Coq 8.9.1 Public
36 Relative prime squares 2019/11/24 20:00:00 3 Coq 8.9.1 Public
35 infinite bool sequence is uncountable 2019/11/24 20:00:00 2 Coq 8.9.1 Public
34 Tree addressing is injective 2019/11/24 20:00:00 2 Coq 8.9.1 Public
33 Constructor is injective 2019/11/24 20:00:00 1 Coq 8.9.1 Public
32 Uniqueness of inequality proofs 2019/10/26 18:00:00 4 Coq 8.9.1 Public
31 Sum of binomial coefficients 2019/10/26 18:00:00 3 Coq 8.9.1 Public
30 Double 2019/10/26 18:00:00 2 Coq 8.9.1 Public
29 Yoneda embedding for preorder 2019/10/26 18:00:00 1 Coq 8.9.1 Public
28 Iterated iteration 2019/10/06 20:00:00 3 Coq 8.9.1 Public
27 Two is not Three 2019/10/06 20:00:00 2 Coq 8.9.1 Public
26 Three is prime 2019/10/06 20:00:00 1 Coq 8.9.1 Public
25 Boolean-hole principle 2019/10/06 20:00:00 1 Coq 8.9.1 Public
24 Multiplication of non-zero value in F_p is injective 2019/09/22 20:00:00 3 Coq 8.9.1 Public
23 Any natural number is expressible in binary notation 2019/09/22 20:00:00 2 Coq 8.9.1 Public
22 De Morgan's laws in Coq 2019/09/22 20:00:00 1 Coq 8.9.1 Public
21 mult_n_O 2019/09/22 20:00:00 1 Coq 8.9.1 Public
20 Grand Garden 2019/09/15 17:00:00 3 Coq 8.9.1 Public
19 unique count 2019/09/15 17:00:00 2 Coq 8.9.1 Public
18 unique (unique l) = l 2019/09/15 17:00:00 2 Coq 8.9.1 Public
17 count l n = count (rev l) n 2019/09/15 17:00:00 2 Coq 8.9.1 Public
16 gcd(n, n+1) = 1 2019/09/15 17:00:00 1 Coq 8.9.1 Public
15 Identity permutation 2019/09/08 20:00:00 3 Coq 8.9.1 Public
14 Multiplication in F_2 is idempotent 2019/09/08 20:00:00 2 Coq 8.9.1 Public
13 Definitions of injectivity 2019/09/08 20:00:00 2 Coq 8.9.1 Public
12 Summand of one 2019/09/08 20:00:00 1 Coq 8.9.1 Public
11 l1 <> l2 if l2 is an odd permutation of l1 2019/08/25 21:00:00 4 Coq 8.9.1 Public
10 Cumulative sum of list 2019/08/25 21:00:00 2 Coq 8.9.1 Public
9 forall l: list nat, l @ [0] <> [] 2019/08/25 21:00:00 1 Coq 8.9.1 Public
8 Equivalent two quicksorts 2019/08/18 16:00:00 4 Coq 8.9.1 Public
7 Product of n consecutive integers is divisible by n! 2019/08/18 16:00:00 3 Coq 8.9.1 Public
6 n < m \/ n = m \/ n > m 2019/08/18 16:00:00 2 Coq 8.9.1 Public
5 n * S m = n + n * m 2019/08/18 16:00:00 1 Coq 8.9.1 Public
4 forall f: bool -> bool, f^3(x) = f(x) 2019/08/18 16:00:00 1 Coq 8.9.1 Public
3 1 + 1 = 2 2019/08/18 16:00:00 1 Coq 8.9.1 Public
2 plus_comm 2019/08/03 09:00:00 1 Coq 8.9.1 Public
1 plus_assoc 2019/08/03 09:00:00 1 Coq 8.9.1 Public