StackRating

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

Anton Trunov

Rating
1532.95 (16,107th) 		Reputation
12,306 (11,942nd)
Page: 1 2 3 ... 8
Title Δ
Why are all numeric literals in Coq showing nat type? +0.44
Would giving up on 'ex falso' change anything w.r.t. depend... -0.05
IndProp: prove that Prop is not provable -0.10
Weak Excluded Middle Implies Morgan law for conjunction 0.00
Does Gallina have an equivalent of Haskell's `$` or Ocaml's... 0.00
How do define a custom induction principle in coq? +0.14
How to bind notation scope to a type 0.00
Coq `ring` tactic with booleans: not a valid ring equation 0.00
How to use Coq arithmetic solver tactics with SSReflect arithmetic... 0.00
Coq proof that p<q or p>=q 0.00
Proving OR is commutative with SSReflect 0.00
Dependent pattern matching - zip two vectors 0.00
How does one approach proving facts about non-primitive recursive f... +0.42
Mutually recursive functions over product type 0.00
How can we define `eqType` for dependent types? 0.00
Coq theorem proving: Simple fraction law in peano arithmetic +0.43
How to handle (let := _ in _) in assumptions 0.00
Coq/SSReflect: How to do case analysis when reflecting && a... -1.88
How to reason across equality proofs? 0.00
Defining recursive function over product type +0.68
How to avoid necessity to put module prefix 0.00
What is the difference between Lemma and Theorem in Coq 0.00
Update single record field in Coq 0.00
How could I make example for sigma type in Coq? 0.00
What are the reserved keywords in Coq? 0.00
Is it possible to prove 'implies_to_or -> de_morgan_not_and_... +0.49
Extracting Prop from Coq to Haskell results in empty type 0.00
How to prove forall (p q:Prop), ~p->~((p ->q) ->p). using... 0.00
Is there some tactic for proving this apparently easy goal? 0.00
Idris - derive extended interface instance -2.02
Can I tell Coq to do induction from n to n+2? -0.57
Uniqueness of majoration proofs +1.86
How does the induction principle for the singleton type unit in Coq... 0.00
Remove All Double Negations in Coq 0.00
Modus Ponens and Modus Tollens in Coq 0.00
Disjunctive Syllogism tactic in Coq? +0.98
Coq:prove Prop implies arithmetic relations of natural number 0.00
Coq define a type constructor for injective functions 0.00
Proving a property on sets 0.00
Prove properties of lists 0.00
Proof generated interactively with :elab doesn't work 0.00
Is it possible to force induction tactic to produce more equations? 0.00
Use False_rec to build an aliased list type in Coq 0.00
VerifiedFunctor - prove map (map g) x = x 0.00
Scopes in Coq - importing without resolution? 0.00
Decreasing argument with dependent types 0.00
How to rewrite: Vect (S (S (n + m))) a -> Vect (S (plus n (S m))... 0.00
Ltac: Matching with ltac on hypothesis which contains user defined... 0.00
Fixpoint with Prop inhabitant as argument +0.42
Turn off automatic induction principle in Coq 0.00