Commit 2019-09-27 14:10 ce7c94fc
View on Github →feat(reduce_projections): add reduce_projections attribute (#1402)
- feat(reduce_projections): add attribute This attribute automatically generates simp-lemmas for an instance of a structure stating what the projections of this instance are
- add tactic doc
- use lean code blocks
- missing
lemma - checkpoint
- recursively apply reduce_projections and eta-reduce structures
- reviewer comments, shorten name new name is simps
- avoid name clashes
- remove recursive import
- fix eta-expansion bug
- typo
- apply whnf to type
- add test
- replace nm by decl_name