mathlib3
feat(tactic): new tactics to normalize casts inside expressions
#988
Merged
Overview
Commits
32
Changes
View On GitHub
Commits
  • new tactics for normalizing casts
    Paul-Nicolas Madelaine committed 6 years ago
  • update using the norm_cast tactics
    Paul-Nicolas Madelaine committed 6 years ago
  • minor proof update
    Paul-Nicolas Madelaine committed 6 years ago
  • minor changes
    robertylewis committed 6 years ago
  • moved a norm_cast lemma
    Paul-Nicolas Madelaine committed 6 years ago
  • minor changes
    robertylewis committed 6 years ago
  • fix(doc/tactics): make headers uniform
    robertylewis committed 6 years ago
  • nicer proof using discharger
    Paul-Nicolas Madelaine committed 6 years ago
  • fixed numerals handling by adding simp_cast lemmas
    Paul-Nicolas Madelaine committed 6 years ago
  • add documentation
    Paul-Nicolas Madelaine committed 6 years ago
  • fixed unnecessary normalizations in assumption_mod_cast
    Paul-Nicolas Madelaine committed 6 years ago
  • minor proof update
    Paul-Nicolas Madelaine committed 6 years ago
  • minor coding style update
    Paul-Nicolas Madelaine committed 6 years ago
  • documentation update
    Paul-Nicolas Madelaine committed 6 years ago
  • Merge branch 'master' into norm_cast
    GitHub committed 6 years ago
  • rename flip_equation to expr.flip_eq
    Paul-Nicolas Madelaine committed 6 years ago
  • update proofs to remove boiler plate code about casts
    Paul-Nicolas Madelaine committed 6 years ago
  • Merge branch 'master' into norm_cast
    Paul-Nicolas Madelaine committed 6 years ago
  • revert to old proof
    Paul-Nicolas Madelaine committed 6 years ago
  • fixed imports and moved attributes
    Paul-Nicolas Madelaine committed 6 years ago
  • add test file
    Paul-Nicolas Madelaine committed 6 years ago
  • new attribute system
    GitHub committed 6 years ago
  • syntax fix
    Paul-Nicolas Madelaine committed 6 years ago
  • change attributes names
    Paul-Nicolas Madelaine committed 6 years ago
  • Merge branch 'master' into norm_cast
    GitHub committed 6 years ago
  • test update
    Paul-Nicolas Madelaine committed 6 years ago
  • small update
    Paul-Nicolas Madelaine committed 6 years ago
  • Merge branch 'master' into norm_cast
    cipher1024 committed 6 years ago
  • add elim_cast attribute
    Paul-Nicolas Madelaine committed 6 years ago
  • add examples for attributes
    Paul-Nicolas Madelaine committed 6 years ago
  • new examples
    Paul-Nicolas Madelaine committed 6 years ago
  • Merge branch 'master' into norm_cast
    GitHub committed 6 years ago
FAQ Terms Privacy Refunds Impressum
Loading