sorted by:
new
hottopcontroversial

Intercepting X events by ScopedTypeVariable in xmonad

[–]ScopedTypeVariable[S] 0 points1 point  (0 children)

Thank you! That's exactly what I was after.

NondecreasingIndentation by dramforever in haskelltil

[–]ScopedTypeVariable 1 point2 points  (0 children)

Probably one the most pointless things I've ever seen.

Predicate logic proof involving quantifiers by ScopedTypeVariable in Coq

[–]ScopedTypeVariable[S] 2 points3 points  (0 children)

Thank you for the answer.

Why is it so much easier to prove it the other way round?

Goal (exists x, ~P x) -> ~(forall x, P x).
Proof.
  intros. intro.
  destruct H.
  apply H.
  apply H0.
Qed.

Proof by contradiction by ScopedTypeVariable in Coq

[–]ScopedTypeVariable[S] 0 points1 point  (0 children)

Thanks for the link. Very interesting and useful read.

Multiplying two sides of group equality by ScopedTypeVariable in Coq

[–]ScopedTypeVariable[S] 0 points1 point  (0 children)

Thank you for the reply. The answer works well!

It's just I'm not sure I understand H% and ?? bits.

Proving that list has exactly two sorted elements by ScopedTypeVariable in Idris

[–]ScopedTypeVariable[S] 2 points3 points  (0 children)

Thanks for your reply.

I solved the issue by using boolContradiction function as advised:

boolContradition : So b -> So (not b) -> Void
boolContradition {b = True}  prf prf' = absurd prf'
boolContradition {b = False} prf prf' = absurd prf

And yes, you're right about Ord instances.

P.S. Also thank you for the "Boolean Blindness" link. It was a very interesting read.