StackRating

An Elo-based rating system for Stack Overflow
Home   |   About   |   Stats and Analysis   |   Get a Badge
Rating Stats for

ejgallego

Rating
1505.40 (133,254th) 		Reputation
5,469 (30,084th)
Page: 1 2 3 4
Title Δ
Stuck in infinite inversion loop Coq 0.00
Problems with dependent types in Coq proof assistant -1.73
Proof involving unfolding two recursive functions in COQ -2.68
Can´t destruct exists in hypothesis 0.00
How is Coq's parser implemented? -2.40
How to define finite set of N elements in Coq? 0.00
Smart modification of Coq environment 0.00
No implicits in dependent "match" pattern with ssreflect 0.00
Adding complete disjunctive assumption in Coq 0.00
How to introduce n distinct symbols in Coq -4.13
How to build a function implicitly in Coq? 0.00
Universe inconsistency (because of strict positivity restriction?) 0.00
How to destruct a exist in goal for coq +3.93
Coq eapply generates a goal with a question mark while proving exis... +3.98
When is the first input to `list_rec` not a constant function? -3.71
How do you selectively simplify arguments to each time a function i... -3.76
Subtyping in Coq 0.00
what does the colon greater than sign mean in coq 0.00
How do I compare two ASCII strings in Coq? +0.21
Getting access to Coq's rich XML-like AST output 0.00
Coq: Proving that the product of n and (S n) is even +1.73
In coq, how to make proofs involving summations and means? 0.00
How to prove the arithmetic equality `3 * S (i + j) + 1 = S (3 * i... -2.45
How to prove uniqueness of a function in Coq given a specification? -4.08
How to apply a rewrite to the right side of a conditional without s... 0.00
How to deal with a function with an exists on the right side? -3.93
Is it possible to rewrite the silly2 example from the Tactics chapt... +3.87
Coq: Simplify (negb (neqb true) to true using "rewrite" o... 0.00
Unfolding a proof term in Coq 0.00
Proof on permutations with Coq proof assistant 0.00
How do Structures with Inheritance (:>) work in Coq? -3.98
Casting types in coq 0.00
can I force Coq to print parentheses? 0.00
Coq notation format for double square braces 0.00
Nonconstructive proofs in Coq? 0.00
Coq variable exists in list +3.86
Coq adding a new variable instead of using the correct one +2.73
Coq: defining more than two mutually recursive functions on inducti... +3.96
Typeclass resolution and autorewrite +4.39
Coq nat type check on match -2.91
'else' in definitions - Coq -3.71
Proof of equality with destructuring let...in -1.36
Are arrows in Coq aliases of universal quantifications? +3.97
Coq: Show all terms in a type or types in a universe in the environ... +4.02
Coq: coercion/subtyping between complex expressions +4.05
Why I can't use a reference type inside a `std::initializer_list` -1.85
Coq inversion tactic that works on the goal? 0.00
Where is the Extensionality of predicates axiom Coq +0.22
What's the difference between logical (Leibniz) equality and lo... +4.43
`No more subgoals, but there are non-instantiated existential varia... -3.65