logic_and_proof icon indicating copy to clipboard operation
logic_and_proof copied to clipboard

Published 20 hours ago • verified publisher icon leanprover

Typo (3.3 Forward and Backward Reasoning)

Open letrec opened this issue 4 years ago • 0 comments

https://github.com/leanprover/logic_and_proof/blob/master/natural_deduction_for_propositional_logic.rst#L432

"or from applying the or-elimination rule to C and C → A" - is it supposed to be "or from applying the implication-elimination rule to C and C → A"?

letrec avatar Apr 19 '20 11:04 letrec