StackRating

An Elo-based rating system for Stack Overflow

Home | About | Stats and Analysis | Get a Badge

Rating Stats for

Vitus

Rating
1583.02 (2,752nd)

Reputation
9,997 (15,278th)

Page: 1 2 3

Title	Δ
Combining proofs of commutativity and associativity of addition	-0.19
How to prove there exist a rational which is less than some rationa...	0.00
Writing Proofs in Agda	0.00
Indentation of modules	0.00
Understanding the syntax of Agda	0.00
Agda type-safe cast / coercion	0.00
universe quantification in agda	0.00
nicer way to write constructors as function in Agda	0.00
Pattern match on specialised constructors	+2.98
Defining a type with a single value	0.00
Making an Agda program output to the console	0.00
"subst" where indices to be equated also use subst	0.00
Can you create functions that return functions of a dependent arity...	+3.21
'let' in record telescope	+3.12
How do I prove a "seemingly obvious" fact when relevant t...	0.00
installing agda fails on duplicate instance declarations	-0.85
Agda 2.4.0.x regression on termination check	0.00
Currying with dependent types in agda	+3.15
Proof in Agda and how to evaluate list based function in C-c C-n	0.00
Assisting Agda's termination checker to make a recursive function	0.00
Agda : Ambiguous name _==_. It could refer to any one of	+1.13
Non trivial negation in agda	+3.24
Merge sort in agda	0.00
Applying rules in Agda	0.00
How to convert number into string in agda?	0.00
Insufficiently evaluated context inside `with` clause	0.00
Agda type error	0.00
Agda: Reading a line of standard input as a String instead of a Cos...	+3.19
Are there propositions that can be proved in classical logic but no...	0.00
Agda Theorems for Powers	0.00
Merge of sorted lists with sized types	0.00
Termination-checking of function over a trie	0.00
Functor instance for Data.AVL	0.00
Level mismatch in Agda	0.00
How to define a singleton set?	0.00
Is the evaluation strategy of Agda specified anywhere?	0.00
Using multiple EqReasoning instantiations conveniently	+3.33
unresolved metas when defining a record in Agda	0.00
Type of a subSetoid	0.00
Indexed family of binary operators with infix notation	0.00
Membership proofs for AVL trees	0.00
Recommended convention for declaring record types for algebraic str...	0.00
Appropriate use of universe polymorphism	0.00
How to prove list split is valid?	0.00
How do I use Agda's implementation of delimited continuations?	0.00
Unresolved meta-variables in equivalence proof	0.00
Instantiating Data.AVL module with different element types	0.00
Agda: Why am I unable to pattern match on refl?	0.00
How dangerous is trustMe?	0.00
What does \forall (∀) actually mean in a signature?	0.00