StackRating

An Elo-based rating system for Stack Overflow

Home | About | Stats and Analysis | Get a Badge

Rating Stats for

Jason Gross

Rating
1544.03 (10,004th)

Reputation
3,985 (42,085th)

Page: 1 2

Title	Δ
What is the meaning of "\|-" in coq, and how do I find the...	0.00
trivial theorem about my inductive type on Coq	-0.40
Syntax error in Coq while reading operator >> =	0.00
Merging hint databases into core	0.00
Coq : How to correctly remember dependent values without messing up...	0.00
How to prove the Equivalence of two object of (proj1_sig f a) and (...	+0.11
IndProp: ev_plus_plus	+3.39
How to eliminate a disjunction inside of an expression?	+3.35
Duplicate subgoals in Coq	0.00
Prove inequality of complex objects	+3.65
How to automatically leverage hypotheses of the form x <> y?	+4.07
How to prove something obviously logical - list_get problem in Prop	0.00
Section mechanism in Coq. Forbid omitting of hypotheses from context	0.00
Assert a proposition on multiple witnesses	0.00
Match context pattern inside a tactic/tactic notation	0.00
Proof with list in Coq	0.00
Extensionally equal predicates and equality of universally quantifi...	0.00
Proving the equality of function application on two equivalent func...	+0.02
tricky dependent pattern match without axioms	0.00
Folding only applications	0.00
A simple case of universe inconsistency	0.00
Prove something is less or equal to other thing using induction in...	+3.70
Proper instance for "nested" matching	0.00
Is there any untyped but valid term in Gallina?	+3.78
Binary search Tree in Coq. Trouble to use ( e0 : (val ?= n) = true...	0.00
Unable to use coq's NDiv after importing	0.00
Coq: Bypassing the uniform inheritance condition	0.00
coq code of the article Homotopy type theory and Voevodsky's un...	0.00
even (n + m) -> even n /\ even m \/ odd n /\ odd m	-0.23
Decomposing equality of constructors with match expressions in Coq	+4.32
Is Z.le as defined in the standard library proof irrelevant?	-4.28
What is the EvalOp in Coq CompCert	0.00
Can `match` be faster than `rewrite`	+4.18
Why isn't Set -> Set : Set?	0.00
Stuck at "Retracting buffer" after type class resolution...	+4.07
Coq Error: There are pending proofs	0.00
Matching with Ltac on a call containing local variable	0.00
View all installed libraries and how they are to be imported in Coq	+3.91
How to write an Ltac to multiply both sides of a equation by a grou...	+3.73
Call a theorem using let-in	0.00
The exact definition of an in built Tactic (case, destruct, inversi...	0.00
On the relative strength of some extensional equality axioms	0.00
Coq: Defining a special function	0.00
Prove theorem with series	0.00
Equality of dependent types and dependent values	0.00
invoke coq typechecker from external programs	0.00
Coq strict positivity is puzzling	0.00
case analysis on evidence of equality type in Coq	-0.02
What is the idiomatic way to get `auto` to perform case analysis?	+4.01
How do we overcome the compile time and runtime gap when programmin...	-3.30