4 ms·

More like coq

• gnulinux 9y ago
  Coq is intuitionistic, classical proofs cannot be expressed. Mathematicians almost always (unless intuitionistic math is your niche) use classical proofs.
  • adamnemecek 9y ago
    It kinda is yes. I don’t understand why classical proofs are still a thing.