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 7 ... 9

Title	Δ
How to use HoTT path induction in Coq?	0.00
How to use Streicher_K_ Axiom	0.00
Equivalent of `remember (f x) as y eqn:H; clear H; clear x`?	0.00
Generalizing a hypothesis when possible	0.00
Using coqide, the command `Require Import BigN` worked using coq 8....	0.00
Subtype with Coq	0.00
Reason for equality definition in COQ and HOTT	+0.47
Is it possible to write C programs using Coq?	0.00
"Ring" tactic in CoqIde not accepted	0.00
Nested recursion and `Program Fixpoint` or `Function`	+1.18
Using eq_refl to get an "x = x" hypothesis	0.00
Coq: Is it possible to prove that, if two records are different, th...	0.00
How does decidable equality works with List.remove?	+0.44
how to figure out what "=" means in different types in coq	0.00
coq induction with passing in equality	-0.05
prove that a list returned from a recursively defined function is f...	0.00
Why can't Coq figure out symmetry of the equality by itself?	0.00
How can I split a list in half in coq?	+0.66
singleton list (`A) in Coq?	0.00
Short(er) proof of `forall n k, (forall q, n <> q * 3) ->...	+0.99
In Coq, how to define a set like A = {x \| f(x) = 0}?	0.00
Proof of the application of a Substitution on a term	-0.06
Check for evars in a tactic that returns a value	-0.40
Canonical structures in ssreflect	0.00
Unknown Interpretation for "_/_" despite importing Arith	0.00
Returning a record from a definition in Coq	0.00
Extracting integer from int_Ring type in mathcomp's ssralg	-0.04
Establish isomorphism between sigma of a prod and disjoint sum	0.00
Proof automation	+0.86
Establish isomorphism between finite natural numbers and sigma	-0.35
Defining different equality types as inductive types in Coq	0.00
Proving isomorphism between Martin-Lof's equality and Path Indu...	0.00
What is Coq's type system doing in this example?	0.00
Messing around with category theory	0.00
Proving constructors are partial functions in Coq	0.00
Coq: destruct (co)inductive hypothesis without losing information	-0.47
Coq: import information about instances	0.00
Raising the failure level of a coq tactic	-0.56
Coq how to target and transform hypotheses to show that they're...	0.00
How to pattern match on a Prop when proving in Coq without eliminat...	0.00
Equality for elements of sig type in Coq	0.00
General Advice about When to Use Prop and When to use bool	0.00
how to prove Theorem 3.5.4 in 《Types and Programming Languages》usin...	0.00
Pattern matching using information from theorems	+1.09
Ltac pattern matching: why does `forall x, ?P x` not match `forall...	+0.43
How to formalize the termination of a term reduction relation in Coq?	0.00
If it is impossible to have O(1) pred on CoC, then why does this wo...	0.00
Idiomatically expressing "The Following Are Equivalent" i...	0.00
Defining a finite automata Coq	0.00
Are constructors in the plain calculus of constructions disjoint an...	0.00