lt_of_le_of_ne{,'}

Stream: general

[Johan Commelin]

Is there any reason for this?

#print lt_of_le_of_ne
-- theorem lt_of_le_of_ne : ∀ {α : Type u} [_inst_1 : partial_order α] {a b : α},
-- a ≤ b → a ≠ b → a < b := _
#print lt_of_le_of_ne'
-- theorem lt_of_le_of_ne' : ∀ {α : Type u} [_inst_1 : partial_order α] {a b : α},
-- a ≤ b → a ≠ b → a < b := _

[Mario Carneiro]

the proof is different, probably

[Kevin Buzzard]

IIRC one uses an axiom

[Kevin Buzzard]

and Kenny wasn't happy

[Kevin Buzzard]

Not all proofs are equal after all!

[Mario Carneiro]

aha

#print axioms lt_of_le_of_ne
-- classical.choice
-- quot.sound
-- propext
#print axioms lt_of_le_of_ne'
-- no axioms

[Johan Commelin]

Aaahrg... I see.

[Johan Commelin]

Ok, I'll be nice, and use the ' version.

[Mario Carneiro]

if you don't care, probably don't bother

[Johan Commelin]

It would be nice if there was a comment explaining this reason in the source (@Kenny Lau, you are missing chances to spread the word)

[Mario Carneiro]

one day the tick will go away and that's one less thing to fix in your proof

[Kevin Buzzard]

an axiomall the axioms

[Kenny Lau]

what is the format of the title of this thread? It doesn't look like regex

[Johan Commelin]

It's a bashism

[Johan Commelin]

mv file.{txt,tex} will do mv file.txt file.tex