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 Δ
Is one being penalized by using 'same_relation' (and possib... 0.00
Best way to handle (sub) types of the form `{ x : nat | x >= 13... 0.00
How do I prove 'S x > 0' from scratch in Coq? -1.90
Proof of idempotence for a function clearing a list but one element -2.85
Nested theorems in Coq 0.00
Refine and @ (at) symbol in Coq 8.5pl1 0.00
Merge duplicate cases in match Coq +4.10
Decomposing equality of constructors coq +0.33
From an Inductive predicate to list A -> list A -> bool +4.30
Weakening hypothesis without a cut -3.71
How to raise exception in Coq?(in match ... end) 0.00
What's the right/left inverse of a function? +1.26
Solving polynomial equation systems in Coq -3.79
Coq fixpoint defintion numerated by natural numbers.(type of (n+1)&... 0.00
eq_rect and natrual type indices 0.00
Coq: cannot find length_zero_iff_nil 0.00
How to destruct/generalize over Program's rewritten match state... 0.00
What prevents Coq from performing a trivial rewrite? 0.00
How to make sublists in Coq? +2.26
Counting number of different elements in a list in Coq -1.81
utop: Error: Reference to undefined global `Grammar' 0.00
Why does this rewrite fail in the context of dependent types 0.00
How to define set in coq without defining set as a list of elements +4.08
Coq syntax for theorem covering cases of negation of and with three... -3.98
Coq tactic that adds the value of an inductive term to the context 0.00
Confused about pattern matching in Record constructions in Coq -0.18
Coq functional extensionality 0.00
Why is Coq prepending "Top." to my terms? 0.00
How do I evaluate a nested match in an assumption that depends on a... -3.89
Is this relationship between forall and exists provable in Coq/intu... +1.42
How to simplify A + 0 > 0 into A > 0? -4.14
Inductive subset of an inductive set in Coq +3.92
Is there a convention for the order of applying ssreflect tactic/ta... 0.00
Does ssreflect assume excluded middle? +4.06
when is the `:` (colon) in necessary in ssreflect/Coq? +3.95
How to find the source file for an identifier in Coq -1.99
How is "less than" defined for real numbers in Coq? -4.14
How to proof in Coq statements about given sets -4.46