StackRating

An Elo-based rating system for Stack Overflow

Home | About | Stats and Analysis | Get a Badge

Rating Stats for

Andreas Lochbihler

Rating
1576.77 (3,311th)

Reputation
4,488 (37,143rd)

Page: 1 2 3

Title	Δ
Initial proof method to consume all incoming facts	0.00
How to use obtain in existential proofs?	+3.33
How to submit an argument to keyword proof?	+4.04
Want to translate syntax "F;" to "True,True,True,Tru...	0.00
Introducing type abbreviations in Isabelle	0.00
Avoid matching (λx.x)	0.00
Custom Isabelle syntax breaks existing syntax	+3.93
Isabelle syntax translations: Force eta-expansion?	0.00
From a 'value' to a 'lemma'	+3.98
let-statement with SOME operator	+3.68
Isabelle: prove that this set notation of a matrice results in a fi...	0.00
proving function definition correctness in Isabelle	+4.10
Unfold/simp has no effect in a primrec type class instantiation proof	0.00
Bad name binding in Isabelle	0.00
Isabelle: Switching between "structured" and "apply-...	0.00
Need proof for meta-logic conjunction elimination rule	0.00
Isabelle: stop simp from splitting a tuple	0.00
Transferring higher order goals	0.00
Isabelle: maximum value in a vector	0.00
Isabelle matrix arithmetic: det_linear_row_setsum in library with d...	0.00
When would you use `presume` in an Isar proof?	0.00
Defining an "arg max" like function over finite sets, and...	+4.03
Inductive Set with Non-fixed Parameters	0.00
What is an Isabelle/HOL subtype? What Isar commands produce subtypes?	0.00
Isabelle's Code generation: Abstraction lemmas for containers?	+4.19
Canonical way to get a more specific lemma	0.00
How can I specify a header and the package of generated code?	0.00
Faster code for 'distinct' on lists	0.00