StackRating

An Elo-based rating system for Stack Overflow

Home | About | Stats and Analysis | Get a Badge

Rating Stats for

Christopher Hughes

Rating
1504.00 (229,416th)

Reputation
76 (841,444th)

Page: 1

Title	Δ
Proving ¬ (A ∧ B) → (A → ¬ B) in Lean	0.00
Quickly simplifying the expression 'ite ("a"="b&...	0.00
Nested pattern matching in Lean for destructing hypothesis	0.00
Proving that two strings are different in Lean	0.00
"failed to synthesize type class instance" in rewrite sub...	0.00
Problem with types in a definition in lean	0.00
prove p or q iff q or p in Lean	0.00
Why was the second inductive hypothesis not needed in this nested i...	0.00
What is the equivalent of Coq's 'fix' keyword to create...	0.00
destruct tactic failed, can only eliminate into Prop	0.00
How to perform multiple exists-eliminations that all share a single...	0.00
How to use `exists.elim` in Lean?	0.00
How can one prove (¬ ∀ x, p x) → (∃ x, ¬ p x) from first...	0.00
Why does `rewrite` of associativity fail in binomial theorem proof...	0.00
How to prove two statements in propositional logic using LEAN?	0.00
How to prove distributivity (propositional validity property 6) in...	0.00
How to prove mathematical induction formulae in LEAN theorem prover?	0.00
Some basic Propositional Logic Proofs in Lean	+4.00
Induction issue	0.00
Simple refl-based proof problem in Lean (but not in Agda)	0.00
Well-founded recursion in Lean	0.00