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 ... 5 6 7 8 9
Title Δ
casting convertible types in coq +0.42
Proving a theorem in Coq using almost only rewrites - no "clev... 0.00
Well founded recursion in Coq -0.34
How to use a custom induction principle in Coq? 0.00
How do I check for convertibility in a tactic producing terms? 0.00
Abstracting over the term ... leads to a term ... which is ill-typed 0.00
How to introduce a new variable in Coq? +0.44
Can destruct used in implication in Coq? 0.00
how to rearrange terms in Coq using plus communtativity and associa... -0.08
Coq: How do I create a bool from a decidable Prop? 0.00
How to make a Coq formalisation reusable? 0.00
Modelling object-oriented program in Coq 0.00
Conversion of nat to Q in Coq 0.00
How do we know all Coq constructors are injective and disjoint? +0.42
How to return a (intro'd) hypothesis back to the goal formula? +0.43
How to show that two variables of inductive type are inequal if the... 0.00
Using lambda in Fixpoint Coq definitions 0.00
Compute with a recursive function defined by well-defined induction 0.00
Incorrect elimination of X in the inductive type "or": +0.46
What does "Error: Universe inconsistency" mean in Coq? 0.00
convoy pattern and match involving inequality 0.00
Coq: manage LoadPath in project with subdirectories +0.45
extracting evidence of equality from match 0.00
Why are logical connectives and booleans separate in Coq? 0.00
Proving False with negative inductive types in Coq 0.00
Making one project a sub-project of another project in coq? 0.00
Formalizing computability theory in Coq +0.50
Tutorial about syntax of HoTT variant of Coq +1.26
Type encapsulation in Coq 0.00
Fail to use let-destruct for tuple in Coq 0.00
Definition by property in coq 0.00
What are the strengths and weaknesses of the Isabelle proof assista... +3.65
How do I write tactics that behave like "destruct ... as"? 0.00
Why can't I define the following CoFixpoint? 0.00
Making and comparing Sets in Coq +3.71
Coq: typeclasses vs dependent records 0.00
Function- and Type substitutions or Views in Coq 0.00
Using Coq Equality Definition 0.00
Expanding Recursive Functions In Coq 0.00
How to choose an element of a stream of unknown size uniformly at r... 0.00
function parameter as json key 0.00
Rewrite tactic fails to find term occurrence within pattern matching 0.00
How to model introduction rule for implication in Coq? 0.00
Software Foundations '|-' notation shadows Ltac match notat... 0.00
Proving equivalence between non-tail-recursive and tail-recursive f... 0.00
Coq Program matching on pair +4.01
Heterogenous list in Coq 0.00
Why is the function addpos defined this way? +4.03
What does positive_to_Qpositive_i in the QArithSternBrocot library... -2.92
How to prove False from obviously contradictory assumptions +5.14