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 6 7 ... 8
Title Δ
A special case of Lob's theorem using Coq 0.00
How does the discriminate tactic work? +0.49
Need help on proving proposition in Coq -0.52
How can I automate counting within proofs in Coq? -0.04
Writing well-founded programs in Coq using Fix or Program Fixpoint 0.00
Multiple Where-clauses for Reserved Notation in Coq? 0.00
Syntax Error with `<` in Coq Notations 0.00
Coq Real numbers -lexing and parsing 3.14 0.00
Supplying section arguments for examples 0.00
How to prove a = b → a + 1 = b + 1 in lean? -0.01
Coq won't compute a typeclass function if the typeclass has a P... 0.00
Coq: Proving an application -1.94
Agda-like programming in Coq/Proof General? +2.90
Why does Lean enforce recursive type arguments to appear after non-... 0.00
How to define mutual inductive propositions in Lean? 0.00
Coq: fixed universe hierarchy w/ explicit universes +0.21
Proper way to use FMap in Coq 8.6? 0.00
How can I read Coq's definition of proj1_sig? 0.00
When is the first input to `list_rec` not a constant function? +0.46
How do you selectively simplify arguments to each time a function i... +0.47
OCAML the record field is not mutable +0.41
Stronger completeness axiom for real numbers in Coq 0.00
How to keep elements in list through out the program in SML? +2.14
How to write coq definitions with "subtypes" 0.00
How to use Coq GenericMinMax to prove facts about the reals 0.00
Idris - Vector Queues and Rewrite Rules 0.00
How do I compare two ASCII strings in Coq? -0.03
Prove that a sequence of steps terminates 0.00
All-quantified type variable in (value) constructor cannot be expli... -0.50
how to find number of occurrences in ML string list? 0.00
Print history list with ocaml utop 0.00
What constitutes a valid type in lean? 0.00
A function of type: ('a -> ('b -> 'c)) -> (... 0.00
Unable to locate library -0.52
Subsets of list nat in coq 0.00
How to replace hypotheses `0 < d` with `S d'` in Coq? 0.00
Function returns string when bool is expected 0.00
How to define a higher-order function which applies a polymorphic f... -1.50
Understanding an SML type fn (f,g,x) => g(f(x)) or similar 0.00
How do I rewrite negb true to false in Coq? +0.46
Stuck on a simple proof about regular expressions +0.47
Coq: Proving that the product of n and (S n) is even +0.74
Coq: Proving that the product of n and (S n) is even +1.61
Coq: Proving that the product of n and (S n) is even -1.14
How to create an field that only accepts other fields? -1.37
Coq's mathematical proof language: Rewriting in if condition +0.47
How to prove the arithmetic equality `3 * S (i + j) + 1 = S (3 * i... +0.47
What is the Emacs keyboard shortcut for the Agda 𝕃 symbol? +2.23
Reduction of terms with fix. (Coq) 0.00
Coq: Remove all (nested) parentheses from a sum +1.87