StackRating

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

chris

Rating
1505.67 (128,546th) 		Reputation
4,510 (36,953rd)
Page: 1 2 3
Title Δ
Writing the list of first n natural numbers as ints in Isabelle -1.91
Locale ignores operation notation 0.00
Isabelle 2017: Support for proof method definitons seems to be... 0.00
Access elements of data types +2.12
How to prove in HOLCF that double reversion of a list doesn't c... 0.00
Very simple lemma in Isabelle 0.00
Definition without recursion, by cases, in Isabelle 0.00
Using an 'if and only if' rule to prove an 'if' sta... -0.48
General way to apply an arbitrary method to all subgoals? 0.00
How to extract concrete values from defined options 0.00
Isabelle recursive function -0.49
Solve ~(P /\ Q) |- Q -> ~P in Isabelle -0.34
Normal constant definition versus lambda constant definition 0.00
Isabelle/HOL foundations -0.01
How to generate code for reverse sorting 0.00
Double function in Isabelle -0.48
Proving a simple arithmetic statement with rewriting in Isabelle +0.49
Converting a set to a list in Isabelle -1.87
Declaring a coercion from a record type 0.00
Isabelle: understanding the use of quantifiers -0.51
Isabelle 'fun' without 'where'? 0.00
Skip a subgoal while proving in Isabelle 0.00
Automata theory and Functional programming 0.00
Isabelle type unification/inference error 0.00
Apply simplifier to arbitrary term -0.45
Why must Isabelle functions have at least one argument? -0.01
Solving equations with an associative and commutative operator -0.46
Proving insertion sort algorithm using Isabelle 0.00
Defining disjoint union of different types in Isabelle and more 0.00
Induction by length and then by an induction rule for context free... 0.00
Function to double a list in Isabelle 0.00
Case names for locale interpretation -0.46
Express that a function is constant on a set 0.00
Calculating transitive closures 0.00
Again, transitive closure and identity 0.00
Transitive closure of identity relation +0.24
Taming meta implication in Isar proofs +0.49
How to define a partial function in Isabelle? -0.30
isabelle proving commutativity for add +0.49
How to streamline a proof of a function property on a datatype? 0.00
Removing repeated elements in lists -0.41
Setting [no_vars] theory-wide +0.11
Custom Isabelle syntax breaks existing syntax -3.93
Remove duplicate but keep the order +3.78
What is inductive predicates? +0.16
From a 'value' to a 'lemma' -3.98
Natural deduction: is this a sound proof? -4.26
Does a list contain alternating elements -4.21
How do I write this function in SML +3.85
How to replace ⋀ and ⟹ with ∀ and ⟶ in assumption +4.00