Def weakLeanArgs

Modification history

2023-12-02 07:05
lakefile.lean
chore: bump Mathlib to Lean v4.4.0-rc1 (#8781) …
Deleted weakLeanArgsView on Github →
2023-09-06 07:39
lakefile.lean
chore: cleanup Mathlib.Init.Data.Prod (#6972) …
Modified weakLeanArgsView on Github →
2023-07-17 23:40
lakefile.lean
fix: make `warningAsError` a weak arg (#5970)
Added weakLeanArgsView on Github →