StackRating

An Elo-based rating system for Stack Overflow

Home | About | Stats and Analysis | Get a Badge

Rating Stats for

Anton Trunov

Rating
1532.95 (16,107th)

Reputation
12,306 (11,942nd)

Page: 1 2 3 4 5 6 ... 8

Title	Δ
How can I create a function that only accepts a subset of construct...	-0.34
How to constraint input type and output type to be the same?	-0.55
Match on existentially hidden type index	0.00
Using sets in lean	0.00
rewrite single occurence in ltac	+0.05
In Coq, How to construct an element of 'sig' type	0.00
How to make use of a hypothesis containing forall in Coq?	0.00
Idris - rewriting in simple theorem proof	+0.46
In Idris, how do I extract a proof from a So type?	+0.46
Ltac : optional arguments tactic	0.00
Ltac: get hypotesis' type from name	0.00
Second order unification with rewrite	0.00
Example uses of MSets in Coq	0.00
Coq best practice: mutual recursion, only one function is structura...	+1.74
Coq Section: require typeclass instance	0.00
Coq: why do I need to manually unfold a value even though it has a...	+0.46
Using TypeClass Instances Within Typeclasses	0.00
Fixpoint functions in Type Class Instances	0.00
How to deal with really large terms generated by Program Fixpoint i...	0.00
Ltac call to "cofix" failed. Error: All methods must cons...	0.00
Coq: usage of `PartialOrder` typeclass	0.00
Idiomatic ways of selecting subterm to rewrite	-0.77
Error message says 'class' is deprecated, source does not c...	0.00
Curry universally quantified function	0.00
How to pull the rhs out of an equality in coq	-0.55
Automatically choose an assumption from local context	0.00
Coq can't compute a well-founded function on Z, but it works on...	0.00
Peano number implementation in Coq	0.00
How to prove that semi-confluence implies confluence in Coq?	0.00
Constants in Idris	+0.47
Cannot guess decreasing argument of fix for nested match in Coq	+0.45
Idris Vect.fromList usage with generated list	0.00
How do I evaluate this recursive function in Idris interactive?	0.00
Coq: goal variable not transformed by induction when appearing on l...	0.00
Coq proof for subtraction does not commute	0.00
Induction over relations	+1.14
How to install SSReflect and MathComp in Linux?	+0.47
Idris: Hiding data types from standard library, or not importing st...	0.00
Idris: totality check fails when trying to re-implement fromInteger...	0.00
Coq losing information from if-statement when doing recursive funct...	0.00
In Idris, use rewrite under a lambda	0.00
In Idris, how do I hide something defined in Prelude?	0.00
Coq rewriting using lambda arguments	0.00
Overloading operators in Coq notations	0.00
Change utop output width	0.00
Views in Idris - Listing 10.5 of Type-Driven Development in Idris b...	0.00
Attaching an attribute to a definition causes syntax errors	0.00
Coq how to pretty-print a term constructed using tactics?	0.00
apply tactic cannot find an instance for a variable	0.00
Idris: How do I rewrite/solve using a 'with' block in a def...	0.00