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 5 ... 8

Title	Δ
How to add variables introduced by set tactic to a Hint DB?	0.00
using user-defined datatype as a type for a function argument	-2.22
Can I prove (s : Stream a) -> (head s :: tail s = s) in Idris?	0.00
Coq: How to apply axioms deeper in the goal?	0.00
How to convert "Zneq_bool a b = true" to a witness of &qu...	0.00
using rewrite in Refl	0.00
How can I prove `false` and by extension anything from Coq hypothes...	+0.46
In Coq, "if then else" allows non-boolean first argument?	0.00
Quicksort in Idris	0.00
How can I write a function of the following form in Coq?	0.00
Prove that the only zero-length vector is nil	-0.54
How can I rewrite selectively in Coq?	0.00
Program Fixpoint: recursive call in `let` and hypothesis of the obl...	0.00
Attempting to use proof irrelevance without creating ill-typed terms	0.00
List uniqueness predicate decidability	-0.55
Using a 3 symbols notation [constr:operconstr] expected after [cons...	0.00
Recovering implicit information from existentials in Coq	+0.09
"Collapsing" state in a functional map?	-0.04
How do I prove the simplified Chinese Remainder Theorem?	-0.07
How to apply Z.divide_add_r in a hypothesis?	+0.19
When destructing fixpoint, add hypothesis without simplifying	0.00
Rewrite hypothesis in Coq, keeping implication	-1.34
How to project (with `proj1` or `proj2`) a universally quantified b...	0.00
How to specify explicit equality in Coq search patterns?	0.00
How does `auto` interract with biconditional (iff)	0.00
not_iff_compat not found in the current environment	0.00
Define product type after importing QArith	0.00
How does the order of implicit arguments affect idris?	0.00
Idris - proving equality of two numbers	+0.45
Nested recursion with partial application	0.00
Coq vector permutations	+0.49
Coinduction on Coq, type mismatch	0.00
Defining the predecessor function (with pred 0 = 0) for the natural...	0.00
Idris - proof on inductive step	0.00
Idris rewrite does not happen	0.00
Why does this 'with' block spoil the totality of this funct...	0.00
Why do these declarations (for the same pattern) satisfy the type c...	+0.45
Non-empty-list comonad	0.00
Is there a more elegant way to write the following Coq code?	+0.46
Eta conversion tactics?	0.00
Idris: Implicit parameters in records	0.00
How to set the module name when extracting Coq to Haskell	0.00
How to rewrite term in type signature for proof in Idris?	0.00
LTE for Integers (ZZ)	0.00
Short(er) proof of `forall n k, (forall q, n <> q * 3) ->...	+0.36
How to import libraries in Coq?	0.00
Totality and searching for elements in Streams	0.00
Proof General complaining script incomplete if running 2 scripts at...	+1.66
Dependent types: Vector of vectors	+0.06
Idiomatic way of listing elements of a sum type in Idris	0.00