New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

INDUCTION PROVE这章里不该是加法交换率而是结合率 #7

Closed

philippica opened this issue Jun 20, 2018 · 1 comment

Labels

bug good first issue

philippica commented Jun 20, 2018

形式化证明 vs. 非形式化证明中：
例如，下面是一段加法交换律的证明：
Theorem plus_assoc' : ∀ n m p : nat,
n + (m + p) = (n + m) + p.

实际应该是结合率，英文原文中也为结合率

liyishuai added bug good first issue labels

liyishuai closed this as completed

Member

liyishuai commented Jun 20, 2018

Should be fixed in r130. Thanks!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment