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 ... 6 7 8 9
Title Δ
Coq QArith division by zero is zero, why? 0.00
Proving a Co-Inductive property (lexical ordering is transitive) in... 0.00
Defining function in Coq 0.00
What is GroupScope? 0.00
Prove a match statement 0.00
In Coq, how do I introduce a variable from an hypothesis into the e... 0.00
Implementing vector addition in Coq 0.00
Eval compute is incomplete when own decidability is used in Coq +3.89
Difference between Definition and Let in Coq 0.00
How to match a "match" expression? 0.00
How to forbid simpl tactic to unfold arithmetic expressions? +3.94
How to do "negative" match in Ltac? 0.00
Stuck in the construction of a very simple function 0.00
What does the perm_invK lemma in Ssreflect prove? 0.00
How to prove functions equal, knowing their bodies are equal? 0.00
Declaring implicit arguments in Coq: how many underscores are needed? -4.11
Unfold anonymous function in Coq proof +3.89
Using contextual information in Coq pattern matching +4.32
How to reference type class-polymorphic variables in a theorem type? 0.00
Defining isomorphism classes in Coq 0.00
Inverting an obviously untrue hypothesis does not prove falsehood 0.00
Using dependent types in Coq (safe nth function) +4.03
Why can't inversion be used on a universally qualified hypothes... 0.00
How can I do intros in a different order without using generalize d... -4.15
Is there a way to prove properties about my C++ programs? 0.00
How to duplicate a hypothesis in Coq? +3.93
Why Coq doesn't allow inversion, destruct, etc. when the goal i... 0.00
How to compile modules inside directories (aka with dots in its name) 0.00
How to prove this simple equation in Coq -4.07
Eliminating cases with propositions in Coq 0.00
Change a function at one point -4.11
Prove equality on Sigma-types 0.00
Apply a function to both sides of an equality in Coq? 0.00
Declaring a well colored digraph in coq 0.00
Dependent type list concatenation in Coq -4.08
Using length of list X as an argument for a constructor of X in Coq 0.00
Coq notation for multi type list +2.22
Counting even number haskell with list comprehension? 0.00
What does `omega` really do here? +4.02
How to build an inductive type for cobordisms using Coq? -0.35
GCD and mod in Coq 0.00
How or is that possible to prove or falsify `forall (P Q : Prop), (... 0.00
Defining a predicate without specifying its truth condition in Coq 0.00
How to prove "~(nat = False)", "~(nat = bool)"... 0.00
Omitting forall in Coq 0.00
Working with semirings in Coq 0.00
What is the idiomatic way to express countable infinity in Coq? 0.00
Defining Unlambda-style tree notation in Coq 0.00
Single-quote notation for characters in Coq? -0.10
Import notation from module signature in implementing module 0.00