Yosuke Ito
I'm using Proof General (Coq) on emacs, and facing a problem. If I do "proof-assert-next-command-interactive" `C-c C-n` after using "I-search" `C-s`, then the proof process gets stuck and never ends....
In the theory `normedtype.v`, we have the lemma `not_near_at_rightP`. The name contains the character `P`, but it states one-direct implication, not the equivalence. For me, this seems contradictory to the...
I am formalizing the cumulative distribution function and related lemmas in `Probability.v`. A possible candidate for the definition is: ``` Definition cdf d (T : measurableType d) (R : realType)...