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 ... 9
Title Δ
Why my way of defining Coercion in this example is wrong, and what... 0.00
Type inequality without cardinality arguments 0.00
Show that a term is not equal to a strictly larger term 0.00
Define sets in a way that equality can be proven by extensionality 0.00
Can I get the successor of an universe in Coq? 0.00
Coq: can I use a type argument as the type of successive argument? 0.00
Non strictly positive occurrence problem in Coq inductive definition 0.00
List of natural numbers in coq 0.00
what is the type of a here 0.00
Generic equality lifting in coq 0.00
How to prove non-equality of terms produced by two different constr... 0.00
Position of elements in list 0.00
Unable to prove that only 0 is less than 1 with mathcomp's finT... 0.00
Proving General Associativity in Groups 0.00
How to prove equality from equality of Some +0.65
Can I use functions in Coq as constructors? 0.00
Theorem on insertion into BST in coq 0.00
Abstracting patterns in induction rule for inductive predicates for... 0.00
Show that a monic (injective) and epic (surjective) function has an... 0.00
How to define an empty set with axiom of subsets in coq 0.00
How can I close this demonstration about opt_c in coq? 0.00
How to prove the same subgoals 0.00
Record, Proof irrelevance, and John Major's equality 0.00
Can you enumerate all values of an inductive type in Coq? 0.00
Dependent type as a function argument in Coq 0.00
Equal indexed inductive types implies equal indices 0.00
Instantiating a commutative ring of Zn with mathcomp 0.00
How to concatenate vectors defined as functions from finite types 0.00
Quantification under sumbool 0.00
Proving that size with filter is not equal to (size + 1) +0.40
Simplifying expression with lists equality 0.00
Coq/SSReflect: How to do case analysis when reflecting && a... +1.88
Why is vm_compute faster in definitions than in proofs in Coq? 0.00
How should a user-defined enumerated type be made `finType`? 0.00
How to use Coq as calculator or as forward chaining rule engine/seq... 0.00
Coq: Proving simple theorem using Fixpoints and Induction 0.00
Simpler proof of `0<a -> 1<a+1` 0.00
How to prove the Equivalence of two object of (proj1_sig f a) and (... -0.01
How can I create a polymorphic "map xs f" function? +0.47
Defining recursive function over product type -1.09
Coq syntax for defining lemmas 0.00
How to guarantee constrained values on a type in Coq? 0.00
How to prove intersection of two non-equal singleton sets is empty 0.00
Have problem with unable to use destruct tatic in a Definition 0.00
Logic: excluded_middle_irrefutable 0.00
Typeclasses with multiple fields vs. single field in Coq / Unexpect... 0.00
What is the standard Cartesian-product construction for Ensemble? 0.00
Import Coq variables from another file +1.91
Why does coq's typechecker reject my map definition? +0.48
Decide disjunctions in sort Prop 0.00