StackRating

An Elo-based rating system for Stack Overflow

Home | About | Stats and Analysis | Get a Badge

Rating Stats for

Anton Trunov

Rating
1532.95 (16,107th)

Reputation
12,306 (11,942nd)

Page: 1 2 3 4 ... 8

Title	Δ
Complete proof that if last list element not in list, prepending wi...	0.00
Defining a pair of cofixpoints by mutual corecursion	0.00
Coq: Stuck using the subtype	-0.09
Wrong Typeclass Instance used in Coq Proof	0.00
Proving the equality of function application on two equivalent func...	-0.00
Tactic to prove a boolean implication	0.00
Coq: Non-list Data structures living in Set?	0.00
Unicity of non-equality proofs	0.00
Unfolding a definition without reduction	0.00
Why, in Coq, a record projection expects a Type as argument?	0.00
Use proof of if expression = true in then part coq	0.00
Apply a function to both sides of equality in a Coq hypothesis	0.00
Can I use a tactics under `coqtop -nois`?	0.00
Coq: cannot unify inductive types	0.00
Equality of cardinalities of two `finType`s with a bijection	0.00
Compute if in a decideable prop in coq	0.00
Comments in _CoqProject	0.00
Installing CoqIDE - Update of jhbuild failed	0.00
Proving if n = m and m = o, then n + m = m + o in Idris?	0.00
Accessors of type class?	0.00
How to prove decidability of a partial order inductive predicate?	-0.72
Applying a Program Definition fails with "unable to unify Prop...	0.00
Can you prove Excluded Middle is wrong in Coq if I do not import cl...	-1.17
setoid_rewrite fails in pattern matching scenario	0.00
In the coq tactics language, what is the difference between intro a...	0.00
(\x=>2.0*x) `map` [1..10] "Can't find implementation fo...	0.00
Coq can't compute well-founded defined with Fix, but can if def...	0.00
make subset types compatible for function application	-0.52
Struggling with functional extensionality	+2.02
Struggling with functional extensionality	+0.35
Theorem Proving in Idris	+0.47
Coq verification of factorial program through two implementations	0.00
Making conclusions based on function output in idris	0.00
Additional pattern matching on the second argument in `plus` for `N...	0.00
Sorted List in Coq	+0.72
unfold notation in ltac	-0.55
Writing proofs of simple arithmetic in Coq	+1.23
Writing proofs of simple arithmetic in Coq	-1.02
How to prove theorem about list of pairs	-0.02
Using Implicit Type Class Parameters in Coq Notation	+0.46
What is eq_rect and where is it defined in Coq?	0.00
Dealing with let-in expressions in current goal	0.00
deriving facts on pattern matching in coq	0.00
`decide equality` for Mutually Recursive Types in Coq?	0.00
Teach coq to check termination	+1.98
How to put things with different type into a list, tagged by string?	-0.05
Type Checking failed when using Dependent Pair	0.00
Dependent Tuple in Idris?	0.00
Coq: automate repeated rewriting	0.00
Finding a well founded relation to prove termination of a function...	0.00