Issues
- 0
Logic and Mechanized Reasoning をリンク集に追加する
#1229 opened - 1
`Delab` の中で dbg_trace を使用すると、エラーだと解釈されてしまう
#1228 opened - 1
`optParam` はデフォルト引数に使われる
#1227 opened - 0
`ring` タクティクの説明を module doc に基づいて更新する
#1226 opened - 0
排中律の二重否定を示す例
#1225 opened - 0
hint タクティクの説明が不完全
#1224 opened - 0
issue テンプレートを消す
#1218 opened - 0
genInjectivity オプションを紹介する
#1217 opened - 0
case タクティクの新しい構文
#1212 opened - 2
帰納法の原理の帰結：`succ` を適用してもループはできない
#1211 opened - 1
帰納法の原理を使って、succ に不動点がないことを示す
#1210 opened - 0
Prop 値構造体を決定可能にする
#1209 opened - 1
MonadTransformer について
#1208 opened - 2
`unsafe` 修飾子を紹介する
#1207 opened - 0
`push_cast` を紹介する
#1206 opened - 0
`StateM` 使用時のよくあるミス
#1205 opened - 0
ring は定数の割り算ならわりと扱える
#1204 opened - 1
- 0
- 0
`qify` のコード例が不適切
#1199 opened - 0
`abbrev` は `@[reducible] def` と同じという主張は根拠がない
#1197 opened - 1
- 2
宣言的コマンドを細かく分類する
#1194 opened - 2
zify を紹介する
#1193 opened - 0
#check コマンドの出力にはデラボレータが使われることを明記する
#1192 opened - 2
aesop 属性を紹介する
#1191 opened - 0
`register_simp_attr` コマンド
#1189 opened - 0
option を自分で定義する例
#1188 opened - 0
排中律があれば free theorem の反例が得られる
#1187 opened - 1
メタプロの本（metaprogramming in lean）の記述が間違っている
#1186 opened - 2
ptrAddrUnsafe に同じものを引数で渡して異なるものが返ってくる例
#1185 opened - 0
rw の制約を追加
#1184 opened - 4
MyNat に対して ring タクティクを作る
#1183 opened - 0
SetLike はなんのためにあるのか
#1182 opened - 0
namespace に対するドキュメントコメント
#1181 opened - 1
List モナドを容易に使用できるようにしたい
#1180 opened - 0
MyNat の eval 結果を数値リテラルとして表示させたい
#1179 opened - 0
- 0
injection タクティクの simp に比べた利点
#1177 opened - 4
`MyNat` に対して `0 ≠ 1` を示すのが面倒
#1176 opened - 2
`[macro_inline]` 属性を紹介する
#1174 opened - 0
`WellFoundedRelation` 型クラスを紹介する
#1172 opened - 1
遅延評価を入れると矛盾が生じる例
#1170 opened - 0
`#test` コマンドを紹介する
#1169 opened - 0
structure のフィールドに型クラスのインスタンスを持たせることができる
#1168 opened - 0
plausible の sampleableExt の実装に対する疑問
#1167 opened - 0
BEq と DecidableEq はどう違うか
#1166 opened - 0
モナド計算の例。自然数リストの積
#1165 opened - 1
プログラムを探索するプログラムを書けるか？
#1164 opened - 1
fold? は有用か
#1163 opened