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

387 Open 518 Closed
387 Open 518 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

Qq ライブラリに言及し、使い方をきちんと説明する 新規項目
#1288 opened Jan 3, 2025 by Seasawher
暗黙の引数を無効にして @ をつけたくなるケースとは？ help wanted Extra attention is needed コード例
#1287 opened Jan 2, 2025 by Seasawher
遅延評価のリスト MLList を紹介する データ型
#1285 opened Jan 2, 2025 by Seasawher
let 式 / let 文 構文・パーサ
#1283 opened Jan 2, 2025 by Seasawher
1
Compiler.IR の読み方 メモ 解決済みにすることを目指さず、残しておくもの
#1282 opened Jan 2, 2025 by Seasawher
Prod.fst や .snd のデラボレータを変更する例 Zulip コード例
#1281 opened Jan 2, 2025 by Seasawher
組み込みの Syntax Category メモ 解決済みにすることを目指さず、残しておくもの
#1274 opened Jan 1, 2025 by Seasawher
Subtype として定義された正の数の集合 Pos の要素を Nat にばらすタクティクの作例 コード例 メタプログラミング
#1273 opened Jan 1, 2025 by Seasawher
1
構造体の定義の曖昧さ問題 バグ・誤り 宣言的コマンド
#1258 opened Dec 31, 2024 by Seasawher
4
dbg_trace の、与えられている変数の名前を表示するような変種 コード例
#1256 opened Dec 30, 2024 by Seasawher
出力サイズをどんどん大きくしたときに、実行時間がどの程度の速度で大きくなるか計測する メモ 解決済みにすることを目指さず、残しておくもの 要調査 さらなる調査を要する
#1254 opened Dec 30, 2024 by Seasawher
1
ring タクティクはなぜ linarith のようにインスタンス引数だけで使えない？ 疑問 最終的には Zulip などで詳しい人に質問すべき
#1250 opened Dec 29, 2024 by Seasawher
#print opaque を紹介する 対話的コマンド
#1249 opened Dec 29, 2024 by Seasawher
構造体に [ext] 属性を付与して、ext タクティクを利用する例がない バグ・誤り
#1243 opened Dec 28, 2024 by Seasawher
Backtrackable メモ 解決済みにすることを目指さず、残しておくもの
#1242 opened Dec 26, 2024 by Seasawher
Type 1 に該当するのは何？ メモ 解決済みにすることを目指さず、残しておくもの
#1240 opened Dec 26, 2024 by Seasawher
proof_wated コマンドの定義 メモ 解決済みにすることを目指さず、残しておくもの
#1238 opened Dec 25, 2024 by Seasawher
ループ計算を表すモナド Zulip メモ 解決済みにすることを目指さず、残しておくもの
#1237 opened Dec 25, 2024 by Seasawher
rw や simp の共通の構文をどう扱うか？ 構文・パーサ 要調査 さらなる調査を要する
#1234 opened Dec 22, 2024 by Seasawher
mdgen のバグで #lint コマンドの出力をアサートできていない バグ・誤り
#1230 opened Dec 22, 2024 by Seasawher
Logic and Mechanized Reasoning をリンク集に追加する 本文
#1229 opened Dec 21, 2024 by Seasawher
Delab の中で dbg_trace を使用すると、エラーだと解釈されてしまう コード例
#1228 opened Dec 21, 2024 by Seasawher
1
optParam はデフォルト引数に使われる メモ 解決済みにすることを目指さず、残しておくもの
#1227 opened Dec 21, 2024 by Seasawher
1
排中律の二重否定を示す例 コード例
#1225 opened Dec 21, 2024 by Seasawher
genInjectivity オプションを紹介する オプション
#1217 opened Dec 20, 2024 by Seasawher
ProTip! Updated in the last three days: updated:>2024-12-31.