Skip to content

Commit

Permalink
Merge pull request #844 from lean-ja/Seasawher/issue835
Browse files Browse the repository at this point in the history
証明無関係の表記揺れ
  • Loading branch information
Seasawher authored Sep 20, 2024
2 parents 4da3262 + ac15538 commit 2a72f8e
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Examples/Type/Prop.lean
Original file line number Diff line number Diff line change
Expand Up @@ -148,7 +148,7 @@ axiom extract_bar : extract bar = -1

-- このとき、以下のように矛盾が得られる
example : False := by
-- 証明無関連により `foo` と `bar` は等しい
-- 証明無関係により `foo` と `bar` は等しい
have irr : foo = bar := by rfl

-- extract が満たすべき条件から、`1 = -1` が導けてしまう
Expand Down

0 comments on commit 2a72f8e

Please sign in to comment.