StackRating

An Elo-based rating system for Stack Overflow

Home | About | Stats and Analysis | Get a Badge

Rating Stats for

Tej Chajed

Rating
1516.37 (40,545th)

Reputation
2,760 (61,181st)

Page: 1 2

Title	Δ
Curry Howard correspondence in Coq	0.00
Avoid printing notation in Coq with Proof General	0.00
Proof Process busy on combine_split	0.00
Can composing try and repeat lead to an infinite loop in Coq?	-3.95
How to turn an single unification variable into a goal, during proof	0.00
How to get coq to print out new goal and hypotheses after applying...	0.00
Hoare triple notation	0.00
Is it possible to get collisions with base64 Encoding / Decoding	0.00
Generalising a set of proofs in coq	0.00
Coq tactic for applying a concrete hypothesis to an existential goal	0.00
How can I give an alias to a type in coq	0.00
Set theory notation with whitespaces and curly braces in Coq	0.00
Is "printf-debugging" possible in Ltac?	0.00
Coq: Rewriting with 'forall' in hypothesis or goal	0.00
Ease life in dependently typed programming using `Function` and `Pr...	0.00
Why does Coq.Init.Logic define the notation "A -> B"?	0.00
Proof that two isomorphic types are different	0.00
Coq: performing inversion on Prop for Set when there is only one case	-4.29
How to make subst keep the prettiest name (minimum one in lexicogra...	0.00
Coq: local ltac definition	0.00
Using backtracking to find value for existential in Coq	0.00
Existential goals are filled in too soon	0.00
Current required number of arguments for unfolding by `simpl`	0.00
Can you find function by type signature in Coq?	0.00
Weird proof obligations resulting from a push/pop evaluator in Coq	+4.19
Rewrite equivalence under exists in goal	0.00
How to extract Coq's Z into Haskell's Integer	0.00
Understanding "well founded" proofs in Coq	0.00
Can you automatically add Haskell import statements when extracting...	0.00
How can I find what file a value is defined in?	0.00
Why FMapAVL usage in argument is non strictly positive while list is?	0.00
how to write to a file, from coq	0.00
Does pointwise decidability imply total decidability?	0.00
define a "dependently typed" module functor	0.00
Efficient Way of Defining Multiple Functions of the Same Type	0.00
What does the Coq command Require Import Ltac do?	0.00
interactive theorem proving with no specified goal	0.00
Ltac: optional variable name	0.00
How to prove the theorems related to updating variables using pairs...	0.00
Polymorph type specification	+3.79
use module signature definition in module implementation	0.00
How to make use of information known about this function type in Coq	+2.67
Is it possible to express a theorem that states which constructors...	0.00
Coq: viewing proof term during proof script writing	+4.42
Extensible tactic in Coq	0.00
How is a .vo file structured so that coqchk may use it?	-4.10
Can I define a tactic under "coqtop - nois"?	0.00
How can I write following inductive proposition in Coq without viol...	0.00
Proof the equal of state in Coq	-0.36
Translate the Maude code into Coq	0.00