lean-ja/lean-by-example

誰かが対応中かもしれないイシューは最後に並べています。 すべて日付順に表示

• 「無名コンストラクタは入れ子になっていても使用できる」は誤り

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  バグ・誤り・不備

  難易度 2/5 1〜3時間 初心者へのやさしさ 65/100

  lean-ja/lean-by-example#2641 · 2026年10月18日 に作成

• FBIP を提案したのは Lean の論文ではない

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 2/5 1〜3時間 初心者へのやさしさ 52/100

  lean-ja/lean-by-example#2640 · 2026年10月4日 に作成

• macro_inline は instance に付けても良い

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 3/5 1〜2日 初心者へのやさしさ 35/100

  lean-ja/lean-by-example#2639 · コメント 1 件 · 2026年10月4日 に作成

• PowerShell の、履歴に基づくサジェストの有効化はいらない

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  バグ・誤り・不備 優先度たかし

  難易度 1/5 1時間未満 初心者へのやさしさ 72/100

  lean-ja/lean-by-example#2638 · 2026年9月28日 に作成

• subset sum 問題の例

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 3/5 1〜2日 初心者へのやさしさ 45/100

  lean-ja/lean-by-example#2637 · 2026年9月20日 に作成

• Updates available but manual intervention required

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  auto-update-lean-fail

  難易度 4/5 3〜5日 初心者へのやさしさ 48/100

  lean-ja/lean-by-example#2636 · 2026年9月17日 に作成

• linear でない使用を検知して警告を出す

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 3/5 1〜2日 初心者へのやさしさ 45/100

  lean-ja/lean-by-example#2633 · 2026年9月11日 に作成

• mkNullNode を使ってコマンドの配列からマクロ生成をする

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 3/5 1〜2日 初心者へのやさしさ 45/100

  lean-ja/lean-by-example#2631 · 2026年9月2日 に作成

• grind funCC の使い方

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  優先度たかし

  難易度 4/5 3〜5日 初心者へのやさしさ 48/100

  lean-ja/lean-by-example#2630 · 2026年9月1日 に作成

• Lean開発者へのインタビュー

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  資料・教材

  難易度 4/5 3〜5日 初心者へのやさしさ 25/100

  lean-ja/lean-by-example#2626 · 2026年8月27日 に作成

• print ボタンを無効にするか、あるいはPDF版をダウンロードするボタンにする

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  バグ・誤り・不備

  難易度 5/5 1週間以上 初心者へのやさしさ 35/100

  lean-ja/lean-by-example#2625 · 2026年8月25日 に作成

• タクティク早見表を独立させる

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  バグ・誤り・不備

  難易度 2/5 1〜3時間 初心者へのやさしさ 45/100

  lean-ja/lean-by-example#2624 · 2026年8月24日 に作成

• recall コマンドを紹介する

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 2/5 1〜3時間 初心者へのやさしさ 65/100

  lean-ja/lean-by-example#2622 · 2026年8月24日 に作成

• method_specs 属性を紹介する

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 3/5 1〜2日 初心者へのやさしさ 25/100

  lean-ja/lean-by-example#2620 · 2026年8月23日 に作成

• Leanの予約語についてのブログ記事

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  資料・教材

  難易度 3/5 1〜2日 初心者へのやさしさ 35/100

  lean-ja/lean-by-example#2617 · 2026年8月21日 に作成

• xs : List α から n 個取り出す組み合わせを全列挙する

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  付録アイデア

  難易度 5/5 1週間以上 初心者へのやさしさ 30/100

  lean-ja/lean-by-example#2616 · 2026年8月21日 に作成

• n の分割を全列挙する

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  付録アイデア

  難易度 3/5 1〜2日 初心者へのやさしさ 55/100

  lean-ja/lean-by-example#2615 · 2026年8月21日 に作成

• CLRS Textbook

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  資料・教材

  難易度 5/5 1週間以上 初心者へのやさしさ 20/100

  lean-ja/lean-by-example#2614 · 2026年8月21日 に作成

• List.product には csimp がある

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  要調査

  難易度 4/5 3〜5日 初心者へのやさしさ 38/100

  lean-ja/lean-by-example#2613 · 2026年8月21日 に作成

• Type上の関数を作る例: asList

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  優先度たかし

  難易度 3/5 1〜2日 初心者へのやさしさ 45/100

  lean-ja/lean-by-example#2612 · 2026年8月20日 に作成

• 有限集合上の自己単射は全射

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 2/5 1〜3時間 初心者へのやさしさ 45/100

  lean-ja/lean-by-example#2611 · 2026年8月18日 に作成

• InfoTreeを紹介する

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  優先度たかし

  難易度 3/5 1〜2日 初心者へのやさしさ 45/100

  lean-ja/lean-by-example#2610 · 2026年8月17日 に作成

• leo によるスライド資料

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  資料・教材

  難易度 5/5 1週間以上 初心者へのやさしさ 25/100

  lean-ja/lean-by-example#2609 · 2026年8月15日 に作成

• Enum Handler

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  付録アイデア

  難易度 4/5 3〜5日 初心者へのやさしさ 35/100

  lean-ja/lean-by-example#2608 · 2026年8月13日 に作成

• 不要な skill を削除する

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  優先度たかし

  難易度 4/5 3〜5日 初心者へのやさしさ 35/100

  lean-ja/lean-by-example#2607 · 2026年8月13日 に作成

• `lia` タクティクを紹介する

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  優先度たかし

  難易度 3/5 1〜2日 初心者へのやさしさ 35/100

  lean-ja/lean-by-example#2606 · 2026年8月13日 に作成

• `omega` ではなくて `lia` を使うよう促すべき？

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  Zulipで質問すべき Zulipで質問済 バグ・誤り・不備

  難易度 3/5 1〜2日 初心者へのやさしさ 45/100

  lean-ja/lean-by-example#2603 · 2026年8月12日 に作成

• FBIPに関する一意性チェックの論文

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  資料・教材

  難易度 5/5 1週間以上 初心者へのやさしさ 25/100

  lean-ja/lean-by-example#2602 · 2026年8月11日 に作成

• 整数係数多項式について

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  資料・教材

  難易度 5/5 1週間以上 初心者へのやさしさ 25/100

  lean-ja/lean-by-example#2601 · 2026年8月11日 に作成

• exists 記号をマクロで出す時の注意点

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 4/5 3〜5日 初心者へのやさしさ 35/100

  lean-ja/lean-by-example#2599 · 2026年8月10日 に作成

• ナップサック問題に対する全探索アルゴリズムを実装し、それが最適解を常に返すことを証明する

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  付録アイデア

  難易度 5/5 1週間以上 初心者へのやさしさ 45/100

  lean-ja/lean-by-example#2597 · 2026年8月7日 に作成

• 接頭辞付きの数値

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  付録アイデア

  難易度 3/5 1〜2日 初心者へのやさしさ 55/100

  lean-ja/lean-by-example#2596 · 2026年8月7日 に作成

• `#time` コマンドが遅いように見えることを注意する

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  バグ・誤り・不備

  難易度 2/5 1〜3時間 初心者へのやさしさ 68/100

  lean-ja/lean-by-example#2595 · 2026年8月7日 に作成

• loogle CLIをLLMに使用させたい

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  Zulipで質問すべき

  難易度 3/5 1〜2日 初心者へのやさしさ 55/100

  lean-ja/lean-by-example#2594 · 2026年8月7日 に作成

• 置換の実装

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  付録アイデア

  難易度 4/5 3〜5日 初心者へのやさしさ 48/100

  lean-ja/lean-by-example#2593 · 2026年8月7日 に作成

• 生文字列リテラルの説明が間違っているかも

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  バグ・誤り・不備

  難易度 2/5 1〜3時間 初心者へのやさしさ 35/100

  lean-ja/lean-by-example#2592 · 2026年8月7日 に作成

• インデントを自動的に除去する生文字列リテラル

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  メタプログラミング 付録アイデア 構文・パーサ

  難易度 5/5 1週間以上 初心者へのやさしさ 35/100

  lean-ja/lean-by-example#2591 · 2026年8月7日 に作成

• #guard_panic コマンドがある

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  要調査

  難易度 2/5 1〜3時間 初心者へのやさしさ 45/100

  lean-ja/lean-by-example#2590 · 2026年8月6日 に作成

• without_expected_type という項構文がある

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  構文・パーサ 要調査

  難易度 4/5 3〜5日 初心者へのやさしさ 35/100

  lean-ja/lean-by-example#2589 · コメント 1 件 · 2026年8月6日 に作成

• public import 等と書かれている部分に hober したらドキュメントを表示する

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  Zulipで質問すべき

  難易度 4/5 3〜5日 初心者へのやさしさ 25/100

  lean-ja/lean-by-example#2588 · 2026年8月6日 に作成

• #eval は式の評価だけをするわけではない

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  バグ・誤り・不備

  難易度 2/5 1〜3時間 初心者へのやさしさ 55/100

  lean-ja/lean-by-example#2587 · 2026年8月6日 に作成

• deprecated package

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  Zulipで質問すべき

  難易度 4/5 3〜5日 初心者へのやさしさ 35/100

  lean-ja/lean-by-example#2586 · 2026年8月6日 に作成

• `Format` を紹介する

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  データ型 優先度たかし

  難易度 2/5 1〜3時間 初心者へのやさしさ 68/100

  lean-ja/lean-by-example#2585 · 2026年8月5日 に作成

• `import Module` の `Module` に hover したときに docstring を見せる

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  Zulipで質問すべき

  難易度 5/5 1週間以上 初心者へのやさしさ 35/100

  lean-ja/lean-by-example#2584 · 2026年8月5日 に作成

• LeanにはHaskellのSTM相当のものがない

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  メモ

  難易度 5/5 1週間以上 初心者へのやさしさ 25/100

  lean-ja/lean-by-example#2583 · 2026年8月5日 に作成

• 山本さんの関数型プログラミングについてのスライド

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  資料・教材

  難易度 3/5 1〜2日 初心者へのやさしさ 35/100

  lean-ja/lean-by-example#2582 · 2026年8月5日 に作成

• Haskellについての山本さんのスライド

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  資料・教材

  難易度 3/5 1〜2日 初心者へのやさしさ 45/100

  lean-ja/lean-by-example#2581 · 2026年8月5日 に作成

• ナップサック問題

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  付録アイデア

  難易度 5/5 1週間以上 初心者へのやさしさ 35/100

  lean-ja/lean-by-example#2577 · 2026年8月3日 に作成

• leanDuction: nested inductive type

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  メモ 資料・教材

  難易度 4/5 3〜5日 初心者へのやさしさ 35/100

  lean-ja/lean-by-example#2576 · 2026年8月3日 に作成

• for ループや while ループに対する intrinsic な不変条件の構文について

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  Zulipで質問すべき Zulipで質問済

  難易度 5/5 1週間以上 初心者へのやさしさ 30/100

  lean-ja/lean-by-example#2575 · 2026年8月1日 に作成