StackRating

An Elo-based rating system for Stack Overflow

Home | About | Stats and Analysis | Get a Badge

Rating Stats for

Arthur Azevedo De Amorim

Rating
1556.89 (6,205th)

Reputation
14,714 (9,614th)

Page: 1 2 3 4 5 6 ... 9

Title	Δ
How can I prove that she cannot prove Or_commutative with only intr...	0.00
Prove a relation is not well-founded	0.00
Understanding compound types in Coq [Software Foundations]	0.00
Proof leaking in Coq extraction?	0.00
Ltac: Matching goal with type that depends on name of previous goal	0.00
Peano arithmetic in Coq	0.00
Deriving a cannonical structure for a record in coq (ssreflect)	0.00
Coq: Nested(?) subtype defining nonzero rational numbers and their...	0.00
Making a term belong to two different types of different hierarchy...	0.00
Ensuring two metavariables aren't unified to the same result	0.00
Defining subtype relation in Coq	0.00
The Coq :> symbol	0.00
Defining the syntax with constraints	0.00
Parametric HOAS in Coq - is it possible to repeat type name inside...	0.00
Difference between sumbool and intuitionnistic disjunction	0.00
How to declare constant of some inductive type in Coq?	0.00
Coq list sorting practices & sortBy?	-0.58
Prove that n < m + n or that 0 < m in COQ	0.00
Dependent Pair Types	0.00
How to prove StronglySorted list consing in coq?	0.00
Record equality in coq	0.00
a function that get the minimum of a set in coq	+1.94
Coq Record Types	0.00
Coq: working with inequalities (<>)	0.00
Coq impact analysis	-0.07
Contradictory hypothesis using coq inversion tactic	0.00
How to represent choice conditions with parameters in Coq	0.00
How to prove decidability of a partial order inductive predicate?	+1.20
Weird proof obligations resulting from a push/pop evaluator in Coq	-0.28
A Coq proof of a theorem which turns a formula containing y into a...	0.00
Non-positive occurrence due to polymorphic function	0.00
Decomposing equality of constructors with match expressions in Coq	-0.54
Understanding Coq through a simple theorem proof	0.00
How to prove that a number is prime using Znumtheory in Coq	+0.43
Coq: viewing proof term during proof script writing	-0.55
Coq: controlling `subst` when we have many equalities	0.00
Induction on record member in Coq?	0.00
What is meant by Coq arrow -> in Coq theorem?	0.00
How can I introduce a non-generalized proposition that is part of a...	0.00
How to prove a theorem on natural numbers using Coq list	0.00
Stuck at "Retracting buffer" after type class resolution...	+0.11
Cannot determine termination	-0.56
Coq: Testing partial convertibilty	0.00
Is it possible to extract the second element of Sigma on the calcul...	0.00
Coq equality implementation	0.00
Tactics with variable arity	0.00
Equality between functional and inductive definitions	0.00
Recovering implicit information from existentials in Coq	-0.09
What are strategies to write large and manageable proofs in Coq?	+0.45
Coq true = false discriminate fails, no primitive equality	-0.57