Skip to content

Issues: lean-ja/lean-by-example

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

542 Open 642 Closed
542 Open 642 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

定義する前からnotation（記法）を使うには メモ 解決済みにすることを目指さず、残しておくもの
#1634 opened Feb 21, 2025 by Seasawher
let 文を展開するような #check コマンドの変種が作れないか？ メタプログラミング 要調査 さらなる調査を要する
#1633 opened Feb 21, 2025 by Seasawher
1
Fin 型を紹介する データ型
#1632 opened Feb 21, 2025 by Seasawher 関数型プログラミング
Formalizing Mathematics2024 資料・教材 情報を得られそうな資料や論文、文献など
#1631 opened Feb 21, 2025 by Seasawher
1
Listのデータ構造としての性質を書く データ型
#1630 opened Feb 21, 2025 by Seasawher 関数型プログラミング
unseal を紹介する 宣言的コマンド 属性 要調査 さらなる調査を要する
#1629 opened Feb 21, 2025 by Seasawher 関数型プログラミング
lemmaではできなくてsimprocが必要な例 メタプログラミング メモ 解決済みにすることを目指さず、残しておくもの
#1628 opened Feb 21, 2025 by Seasawher
1
遅延評価型のリストを調査する データ型 要調査 さらなる調査を要する
#1627 opened Feb 20, 2025 by Seasawher 関数型プログラミング
section .. end とかの囲う系のコマンドは別にするか？
#1626 opened Feb 20, 2025 by Seasawher
RandMについて調査する データ型
#1625 opened Feb 20, 2025 by Seasawher 関数型プログラミング
by_cases はマクロ タクティク
#1624 opened Feb 20, 2025 by Seasawher
モナドに包まれていないことを「純粋」って呼ぶのわかりにくくないか？ メモ 解決済みにすることを目指さず、残しておくもの
#1623 opened Feb 20, 2025 by Seasawher
正規表現実装の論文 資料・教材 情報を得られそうな資料や論文、文献など
#1622 opened Feb 20, 2025 by Seasawher
#evalと#reduceの違い/#reduceはToExprを使う 要調査 さらなる調査を要する
#1621 opened Feb 20, 2025 by Seasawher
2
lake updateが遅いのでprogressを表示してほしい 要調査 さらなる調査を要する
#1620 opened Feb 20, 2025 by Seasawher
exact? はローカルで勝手に作った定理も提案してくれる タクティク
#1619 opened Feb 20, 2025 by Seasawher
Haskell wiki Traversable 資料・教材 情報を得られそうな資料や論文、文献など
#1617 opened Feb 18, 2025 by Seasawher
simp の代わりに明示的に rw を使いたくなる状況の例 コード例 タクティク
#1616 opened Feb 18, 2025 by Seasawher
simp は等式しか扱えないわけではない コード例 タクティク
#1615 opened Feb 18, 2025 by Seasawher
1
拡張可能な contradiction タクティク 要調査 さらなる調査を要する
#1614 opened Feb 18, 2025 by Seasawher
1
両側辞書 要調査 さらなる調査を要する
#1613 opened Feb 18, 2025 by Seasawher
ロケール付き数値
#1612 opened Feb 18, 2025 by Seasawher
ディレクトリの dir._root_.lean ファイルは import dir で読み込めるようにする 要調査 さらなる調査を要する
#1611 opened Feb 18, 2025 by Seasawher
帰納的述語の例。ライブラリにおけるNat.le メモ 解決済みにすることを目指さず、残しておくもの 型システム 宣言的コマンド
#1610 opened Feb 18, 2025 by Seasawher
a ≦ b と ∃k, a + k = b が同値という命題がライブラリにない？ 要調査 さらなる調査を要する
#1609 opened Feb 18, 2025 by Seasawher
ProTip! Mix and match filters to narrow down what you’re looking for.