Mathlib v3 is deprecated. Go to Mathlib v4

Structure foo

Modification history

2020-11-03 17:56
test/mk_iff_of_inductive.lean
feat(tactic/mk_iff_of_inductive_prop): mk_iff attribute (#4863) …
Added fooView on Github →
2020-05-29 16:24
test/protec_proj.lean
feat(tactic/protect_proj): protect_proj attribute for structures (#2855) …
Added fooView on Github →
2020-04-07 06:44
test/refine_struct.lean
fix(tactic/refine_struct): don't add unnecessary `eq.mpr` or `id` (#2319) …
Added fooView on Github →
2019-11-07 03:43
test/tactics.lean
feat(extensionality): rename to `ext`; generate `ext` rules for structures (#1645) …
Added fooView on Github →