Search results

提案: Option を Except に橋渡しする実践例 (getDM と let some := ... | throw)

codex-automation

Status: Open.

#2449 In lean-ja/lean-by-example;

· Seasawher opened on Jun 15, 2026

r# 構文を紹介する

Status: Open.

#2447 In lean-ja/lean-by-example;

· Seasawher opened on Jun 14, 2026

STを使ってFalseを示す例

Status: Open.

#2442 In lean-ja/lean-by-example;

· Seasawher opened on Jun 11, 2026

Girard のパラドックスの説明に使った証明に図を添付する

Status: Open.

#2441 In lean-ja/lean-by-example;

· Seasawher opened on Jun 11, 2026

付録アイデア。誤り訂正符号

付録アイデアEXTRA/ 配下にあるファイルを付録というが、ここに追加したいアイデアEXTRA/ 配下にあるファイルを付録というが、ここに追加したいアイデア

Status: Open.

#2440 In lean-ja/lean-by-example;

· Seasawher opened on Jun 11, 2026

Decidable 型クラスはなぜTypeに属するのですか？Propだと何が困るのですか？

Status: Open.

#2439 In lean-ja/lean-by-example;

· Seasawher opened on Jun 10, 2026

嫉妬深い夫たちのパズルは、Finの利用例でもある

Status: Open.

#2436 In lean-ja/lean-by-example;

· Seasawher opened on Jun 10, 2026

カッコ式のパーサーを実装する

付録アイデアEXTRA/ 配下にあるファイルを付録というが、ここに追加したいアイデアEXTRA/ 配下にあるファイルを付録というが、ここに追加したいアイデア

Status: Open.

#2435 In lean-ja/lean-by-example;

· Seasawher opened on Jun 10, 2026

Monad を opaque で与えておいて、do 構文を reduce するか print する

Status: Open.

#2434 In lean-ja/lean-by-example;

· Seasawher opened on Jun 9, 2026

付録アイデア。macro expand を行う

Status: Open.

#2433 In lean-ja/lean-by-example;

· Seasawher opened on Jun 9, 2026

image をTypstで生成する

Status: Open.

#2432 In lean-ja/lean-by-example;

· Seasawher opened on Jun 9, 2026

grind に「準同型性」を扱わせる例

Status: Open.

#2430 In lean-ja/lean-by-example;

· Seasawher opened on Jun 9, 2026