StackRating

An Elo-based rating system for Stack Overflow
Home   |   About   |   Stats and Analysis   |   Get a Badge
Rating Stats for

ejgallego

Rating
1505.40 (133,254th)
Reputation
5,469 (30,084th)
Page: 1 2 3 ... 4
Title Δ
How to realize open formula in Coq? -0.51
Removing tcast from tuples... Season 2 0.00
coq 8.11.0 incompatible with ocaml 4.10? 0.00
Prove equality on list constructed with a map -1.01
What does plus '+' operator mean between two propositions i... 0.00
How do I describe a multiplication of vectorized matrices? 0.00
How to prove equality from equality of Some -1.13
How to extend a grammar in coq? 0.00
Discriminate goal in Coq -0.51
Defining intersection types in Coq 0.00
Reasoning with pattern matchings in Coq 0.00
How do destruct list in Coq (nil or not nil) +0.50
What is the difference between definitions and theorems? +2.21
How to show injectivity of a function? 0.00
Check less or equal natural number in coq +0.51
get field from Record Types in Coq -0.03
How to assert (H4: [] = [] ++ []) in a coq problem when there is no... -1.75
Inspecting elements of an inductive type from OCaml 0.00
Coq: unfold tricky notations -0.46
How to upgrade Ocaml to the latest version to support QuickChick in... -0.46
Use condition in a ssreflect finset comprehension 0.00
apply rewrite tactic to sub-expression +0.70
What is the case_eq equivalent of the induction tactic? 0.00
Lemma about maximum, induction on natural numbers in Coq 0.00
Intersection of lists using List.filter 0.00
Searching a list by List.filter 0.00
How to find difference between two lists in coq +0.24
Uniqueness of majoration proofs -1.86
What are standard practices for developing Coq code in Atom Editor? 0.00
How to install Proof General for Emacs on Mac? -0.02
Construct a new record instances when the Record type has dependent... 0.00
Non-empty list append theorem in Coq -0.52
Characteristic function of a union +2.77
Coq tactic to sort a list? -0.33
Having trouble with inequalities with rational numbers 0.00
Coq: (a :: L1) = (b :: L2) ⇒ a = b ∧ L1 = L2? 0.00
Coq: unfold all Definitions 0.00
Finite list with unknown size 0.00
Equality of finite maps in coq (defined using map2) +0.50
CoqIde strange message upon auto tactics 0.00
How to prove the inductive step in coq? -0.04
Reasoning about the boolean vector in Coq, based on the value of it... +0.48
Subtyping using ssreflect 0.00
Why are the real numbers axiomatized in Coq? -1.77
Coq: Stuck using the subtype +0.06
Minimum in non-empty, finite set +0.47
Diffent versions of same library in Coq +0.46
Can you prove Excluded Middle is wrong in Coq if I do not import cl... +2.17
Boolean equality of lists in Coq? +0.49
Coq Reals and Ssreflect GRings 0.00