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 ... 9
Title Δ
Proofs' role in Coq extractions +2.21
Logic: All_In can't expand nested forall 0.00
Logic: In_example_2 0.00
Tactics: stuck in eqb_trans 0.00
universe inconsistency with sumbool 0.00
Proving that a rational function is monotonically nondecreasing in... 0.00
Why does nesting the induction tactic also nest the inductive hypot... 0.00
I'm looking for this lemma about the nat type +0.04
Using "omega" for type "N" 0.00
Proving (~A -> ~B)-> (~A -> B) -> A in Coq 0.00
Recursion for Church encoding of equality 0.00
How do I use a lemma from a Coq library? 0.00
"if" is not just sugar for "match" 0.00
Prove a property of finding the same elements in two lists 0.00
What <> is in Coq -0.05
How to define axiom of a line as two points in Coq 0.00
Learning coq, not sure what the error means NNPP 0.00
Curly brace in Coq generics 0.00
Using induction starting from 1 in Coq 0.00
Extract / use membership proof from a ssreflect finset 0.00
Derive a ssreflect finType from a seq over a finType with uniq 0.00
Destructing equality of dependent records in coq 0.00
Proof (not-quite) irrelevance when when destructing coq equality 0.00
Coq fails an apply tactic +0.40
Injectivity of successor of natural numbers in Coq 0.00
Cannot Unify two hypotheses which are identical 0.00
How to find difference between two lists in coq -0.24
What does it mean when you have multiple lines defining the action... 0.00
Coq: Unable to Unify 0.00
Preserving structure with inductions on 2 variables +0.42
Using functions in definitions 0.00
Recursion in the calculus of construction 0.00
Using the same proof for two subgoals in Coq 0.00
Defining equality relation for infinite trees -0.55
Disjunction Commutavity in Coq 0.00
renaming part of hypothesis in Coq -0.57
Proving theorems about inductive types using _ind; App rule 0.00
How to use "field" with rationals? 0.00
When are the constructors of an inductive type exhaustive? 0.00
How to put 'a is a subset of b'in coq? 0.00
Proving a property of Subset relation on list of pairs 0.00
Path induction using eq_rect 0.00
How to prove decidability of a relation swaping its parameters? +0.47
Why can IHn' (n' = n' + 0) from induction be used to pr... 0.00
How to prove that terms of a first-order language are well-founded? 0.00
Cardinality of Prop, Set and Type_i in Coq 0.00
How to do higher-order term rewriting in Coq? 0.00
Coq: matching inside Inductive definition 0.00
Understanding COQ proof on Show Proof. 0.00
Why are the real numbers axiomatized in Coq? +1.77