Zulip Chat Archive
Stream: new members
Topic: unnecessary axioms
Nick Chopper (Mar 28 2020 at 12:40):
it seems that nat.lt_of_sub_pos
in mathlib can simply call nat.add_lt_of_lt_sub_left
to avoid use of classical.choice
Nick Chopper (Mar 28 2020 at 12:41):
(deleted)
Patrick Massot (Mar 28 2020 at 12:41):
If you care about avoiding choice you can open a PR.
Kevin Buzzard (Mar 28 2020 at 12:45):
Mathlib has become a classical library for the most part
Patrick Massot (Mar 28 2020 at 12:49):
But he can still open a PR if he cares, right? Certainly I won't fix this because I don't care using choice, but that modification doesn't sound like it would make mathlib more difficult to use.
Nick Chopper (Mar 28 2020 at 13:00):
Not worry much about that... just want to follow https://arxiv.org/abs/1904.09193 with Lean (and avoid classical reasoning at this time)
Mario Carneiro (Mar 28 2020 at 22:20):
You can just use your own version of lt_of_sub_pos
if you want it in your local proof
Mario Carneiro (Mar 28 2020 at 22:20):
if it has ended up deeply embedded as a result of, say, the proof that int
is a ring, then you will need to PR to fix that
Last updated: Dec 20 2023 at 11:08 UTC