Mathlib v3 is deprecated. Go to Mathlib v4

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

Estimated changes

added structure automorphism_plus_data
added def bar
added def baz
added structure equiv
added structure equiv_plus_data
added def foo.bar1
added def foo.bar2
added def foo.foo
added def my_equiv
added def name_clash
added def name_clash_fst
added def name_clash_snd
added def name_clash_snd_2
added structure partially_applied_str
added def refl_with_data'
added def refl_with_data
added def test
added def dummy
added structure equiv
added structure my_str
added def right_param
added def wrong_param