StackRating

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

user9716869 - supports Ukraine

Rating
1504.51 (155,673rd) 		Reputation
562 (248,821st)
Page: 1 2
Title Δ
How does an empty pair of "proof qed" work in Isabelle? 0.00
What is the main symbol in Isabelle's set operator (‘) :: ('... 0.00
How to get ML values from HOL? 0.00
How to refer to variables in induction 0.00
How can I prove "(⋀x. PROP ?P x) ⟹ PROP ?P ?x" in Isabelle? 0.00
Proving two bindings equal in Nominal Isabelle 0.00
Is rule method with assumption discharge deprecated in Isabelle? 0.00
Defining function with several bindings in Isabelle 0.00
Diagonalising a finite set of infinite sets 0.00
How do I prove that an object does not interpret a locale? 0.00
What are the semantics of assume for Isabelle/Isar? 0.00
Why can't I apply a single step of a function like I do with de... 0.00
What is wrong with this Isabelle proof? 0.00
Proof over cases for which set element is included in 0.00
How to prove this simple theorem in Isabelle? 0.00
Using an inverse value of an injective function -2.55
Case analysis on function definition in Isabelle -0.08
How to apply standard to all subgoals in Isabelle? 0.00
Using the type-to-sets approach for defining quotients 0.00
How does one insert values into unknowns in isabelle theorem prover? +3.53
Focussing on new subgoals in Eisbach +3.61
Isabelle/HOL restrict codomain 0.00
Extracting BNF data in Isabelle 0.00
Exploring ML files in Isabelle 0.00
Debugging ML proofs in Isabelle 0.00
Fix a field with characteristic different from 2 in Isabelle 0.00
Defining function over equivalence classes Isabelle 0.00
Proving existence in Isabelle/HOL in this example 0.00
Using prefer_tac correctly 0.00
Isabelle's document preparation 0.00
Gather all non-undefined values after addition 0.00
Why is Isabelle/HOL 2018 showing error without error message? 0.00
Refining a definition in Isabelle 0.00
Find the instantiation of a class for a type 0.00
Casting int to nat in Isabelle 0.00
Simplify only using one definition 0.00
Type variable as locale 0.00
A quick way to arrive to the abelian group of order eight in Isabelle 0.00
How to pass assumptions to interpretation of locale 0.00
Can I construct a while structure algebraically using class and loc... 0.00
membership proof 0.00
Induct on two variables? 0.00
Unable to figure out induct rule for mutually recursive predicates 0.00
What does Metis: Unused theorems mean in this context? 0.00
How to lift a transitive relation to finite maps? 0.00
Pull all occurrences of the induction variable into the conclusion... 0.00
How to define a termination order for the function with fmmap_keys? 0.00
Proving the correctness of an algorithm to partition lists in Isabe... 0.00
Reasoning about overlapping inductive definitions in Isabelle 0.00
How to lift a transitive relation from elements to lists? 0.00