Stream: new members
Michael Beeson (Nov 25 2020 at 19:49):
h6: ¬¬(Nc M (Φ M (𝕋 M m)) = two ∨ Nc M (Φ M (𝕋 M m)) = three)
Then push_neg at h6 removes the double negation, instead of just pushing one negation. Up until now, I have never seen
push_neg take an intuitionistically incorrect step. Now I need to be triple-vigilant to check the axioms used in my proofs.
Too bad about this as offhand I do not know how to push just the one negation.
Ruben Van de Velde (Nov 25 2020 at 20:18):
Perhaps the documentation should be clearer on that
Johan Commelin (Nov 25 2020 at 20:24):
@Michael Beeson I am afraid that you are fighting uphill, because mathlib is very decidably classical. Supporting intuitionistism is not on one of our priorities, and hence we also don't point out every occurence of classical or intuitionistic arguments.
Yakov Pechersky (Nov 25 2020 at 20:25):
Maybe use the lemmas that do the rewriting instead of
Last updated: May 15 2021 at 00:39 UTC