7.4章 do (#67)

* 翻訳開始 * 和訳完了 * ビルドエラー修正記載微修正 * セルフレビュー
lean-ja · Aug 25, 2024 · b7e9ee0 · b7e9ee0
1 parent b3bc698
commit b7e9ee0
Show file tree

Hide file tree

Showing 3 changed files with 360 additions and 3 deletions.
diff --git a/examples/early-return/EarlyReturn.lean b/examples/early-return/EarlyReturn.lean
@@ -50,6 +50,6 @@ theorem mains_match : main = Nested.main := by
   simp [main, Nested.main]
   simp [bind, EStateM.bind, EStateM.pure, liftM, monadLift, pure, ite]
   funext s
-  repeat split <;> try simp
+  repeat split <;> try simp_all
   cases argv <;>
-    simp [instDecidableEqString, instDecidableEqList, List.hasDecEq, bne, BEq.beq, List.beq, not, instDecidableEqBool, Bool.decEq]
+    simp [instDecidableEqString, instDecidableEqList, List.hasDecEq, bne, BEq.beq, List.beq, not, instDecidableEqBool, Bool.decEq, IO.FS.Stream.putStrLn, IO.FS.Stream.putStr, String.push, String.decEq, String.trim, instDecidableNot, *]
diff --git a/functional-programming-lean/src/SUMMARY.md b/functional-programming-lean/src/SUMMARY.md
@@ -49,7 +49,7 @@
   - [IOとReaderを組み合わせる](monad-transformers/reader-io.md)
   - [モナド組み立てキット](monad-transformers/transformers.md)
   - [モナド変換子の順序](monad-transformers/order.md)
-  - [More `do` Features](monad-transformers/do.md)
+  - [さらなる `do` の機能](monad-transformers/do.md)
   - [Additional Conveniences](monad-transformers/conveniences.md)
   - [Summary](monad-transformers/summary.md)
 - [Programming with Dependent Types](dependent-types.md)