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	Δ
Using a definition to produce an specific example of a locale in Is...	0.00
Should I use universal quantification in lemma formulation?	0.00
Instances in locale declaration for Isabelle	0.00
Using syntax/translations wiith locales	0.00
Quotienting a mutually recursive family of datatypes	0.00
Using the ordering locale with partial maps	0.00
Avoiding assumption with sledgehammer	0.00
Automatically unfolding a record definition when accessor is used	0.00
Instantiating variables ending in a digit using where-attribute (Is...	0.00
How can I use proved goals of locale interpretation to prove the re...	0.00
Isabelle: linord proof	0.00
Termination proof with functions using set comprehensions	0.00
Simplify expressions with nested ∃ and an equality	0.00
Isabelle - Nitpick counterexample usage	0.00
Isabelle failed to finish proof even though this is same as goal	0.00
How to fix "Illegal schematic variable(s)" in mutually re...	0.00
How to declare "free" instance of type class?	0.00
Set of tuples in Isabelle	0.00
Isabelle: Class of topological vector spaces	0.00
How to ensure that instantiations of type variables are different	0.00
Bad theory import in isabelle	0.00
Isabelle: new axiom for undefined functions	0.00
hiding operators to avoid ambiguities in the AST	+3.29
Using type classes to overload notation for constructors (now a nam...	0.00
Existing constants (e.g. constructors) in type class instantiations	0.00
Variable arity function in Isabelle	+3.37
Rewriting with non-equality equivalence-relations using Isabelle si...	+3.44
Isabelle: locale interpration about record fails in proof	0.00
Refining a Isabelle type declaration	0.00
Why won't simp handle this term inside of a lambda expression?	0.00
In isabelle, why is this simplification lemma not being substituted?	0.00
Make automatic termination proof use different size function	0.00
Create a quotient-lifted type with polymorphism over working set an...	0.00
Substituting for the lambda expression in Isabelle	-0.57
Apply simplifier to arbitrary term	+3.58
How to get the value of a const with ML code in Isabelle?	+3.52
Solving equations with an associative and commutative operator	+3.67
"invalid map function" when defining a corecursive tree	0.00
How to define Subtypes in Isabelle and what they mean?	0.00
Untyped set operations in Isabelle	0.00
How type casting is possible in isabelle	0.00
Can I "map" an "OF" over a list of lemmas	0.00
Predefined functions for Binary trees in Isabelle	0.00
Case names for locale interpretation	+3.72
Fixing type variables in locale extensions	0.00
Infix relation transformer syntax in Isabelle	0.00
How to define a partial function in Isabelle?	+3.76
How to use single-valued relations to rewrite a goal automatically?	0.00
proof (intro ..., elim ...) with multiple goals	0.00
Solve equations involving “obvious” set operations	0.00