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.

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

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

Issues list

inductive type のスタイル校正
#1408 opened Jan 29, 2025 by Seasawher
docComment を紹介する 修飾子
#1395 opened Jan 28, 2025 by Seasawher
[delab] 属性を紹介する 属性 要調査 さらなる調査を要する
#1393 opened Jan 28, 2025 by Seasawher
universe コマンドを紹介する 宣言的コマンド 要調査 さらなる調査を要する
#1392 opened Jan 28, 2025 by Seasawher
simp_all で示せなくて simp at * では示せる例 コード例 タクティク 準備完了 執筆のための調査が終わっていて、執筆できる状態
#1387 opened Jan 26, 2025 by Seasawher
公理がどこで導入されたかまで出力する #print axioms コマンドの亜種 コード例 メモ 解決済みにすることを目指さず、残しておくもの 対話的コマンド
#1383 opened Jan 24, 2025 by Seasawher
[memo] 属性を自作して自動でメモ化を行う例 コード例 メモ 解決済みにすることを目指さず、残しておくもの 属性
#1382 opened Jan 24, 2025 by Seasawher
toString の代わりに reprStr を挿入する d! マクロを自作する例 コード例 構文・パーサ 準備完了 執筆のための調査が終わっていて、執筆できる状態
#1381 opened Jan 24, 2025 by Seasawher
末尾再帰を紹介する 慣習 要調査 さらなる調査を要する
#1379 opened Jan 24, 2025 by Seasawher
ProTip! Type g p on any issue or pull request to go back to the pull request listing page.