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 Δ
Coq proof that complement is involutive 0.00
Consistency of Inductive propositions 0.00
Do not import notations in coq 0.00
Proof in coq - Predicate logic +0.49
instantiate parameters to evaluate function definitions 0.00
Sorted List in Coq -1.19
What are background goals, shelved goals, and abandoned goals in Coq? 0.00
How to make use of information known about this function type in Coq -0.48
refining types with modules and typeclasses 0.00
How is a .vo file structured so that coqchk may use it? +0.51
case analysis on evidence of equality type in Coq +0.00
Computing with a finite subset of an infinite representation in Coq -0.10
How can I write a function in Coq which given a list returns smalle... 0.00
How to partition Coq code to feed Coq ideslave (XML protocol)? 0.00
Is ssrnat included in Coq 8.7? 0.00
Coq XML Protocol: a likely PrintAST malfunction 0.00
what is the "editId" in Coq's XML Protocol document? +0.49
Coq Index Relation 0.00
How we can access Coq or Isabelle/HOL using python program? -0.20
Rewrite hypothesis in Coq, keeping implication +0.93
Coq : simulate function extensionality theorem 0.00
Creating a dictionary/map in Coq -0.51
Using destruct on pattern match expression with 'convoy pattern... 0.00
How to define the basic data types such as Boolean, Interger in Coq 0.00
Obtain decidable total order on a type from an injection into `nat` 0.00
Tactic automation: simple decision procedure -0.17
Tactic automation: simple decision procedure -0.17
Coq: How to prove if statements involving strings? +0.51
Coq: How to prove max a b <= a+b? 0.00
Prove existential quantifier using Coq +0.54
How does elim work in Coq on /\ and \/? 0.00
Why would the tactic 'exact' be complete for Coq proofs? +0.51
How can I match on a specific value in Coq? 0.00
coq What tactics should I use forall A : Prop, A -> ~~A +0.51
Short(er) proof of `forall n k, (forall q, n <> q * 3) ->... -1.11
How to call proof asistant Coq from external software +0.49
Trouble with Coq type classes when defining recursive dependent fie... 0.00
How to do induction on the length of a list in Coq? -0.49
Establish isomorphism between finite natural numbers and sigma +4.20
Dependent pattern matching on two values with the same type -0.19
Coq: rewrite preserving input hypothesis 0.00
Automation of ssreflect, Coq while dealing with contradicted hypoth... 0.00
Coq: destruct (co)inductive hypothesis without losing information +4.56
Ordered seq in Coq/SSreflect 0.00
Idiomatic ways of selecting subterm to rewrite -1.15
How to pull the rhs out of an equality in coq +4.41
Coq - Proving condition about elements of sequence in Ssreflect 0.00
Coq - proof over empty range in Ssreflect 0.00
Coq - Proving strict inequality involving bigops in Ssreflect 0.00
Coq - dependent type error in rewrite 0.00