Skip to content
This repository has been archived by the owner on Oct 14, 2023. It is now read-only.

various additions #605

Merged
merged 17 commits into from
May 18, 2015
Merged

various additions #605

merged 17 commits into from
May 18, 2015

Commits on May 16, 2015

  1. fix(library/data/{set,finset}/basic.lean: delete \{{ \}}} notation (c… 

    …onflicts with records)
    @avigad
    avigad committed May 16, 2015
    Configuration menu
    Copy the full SHA
    81d0d4a View commit details
    Browse the repository at this point in the history

  2. fix(library/algebra/order.lean): rename decidable_eq to had_decidable… 

    …_eq to avoid conflict
    @avigad
    avigad committed May 16, 2015
    Configuration menu
    Copy the full SHA
    daf53e4 View commit details
    Browse the repository at this point in the history

  3. fix(library/data/fintype.lean): reduce imports, to avoid cyclic depen… 

    …dencies
    @avigad
    avigad committed May 16, 2015
    Configuration menu
    Copy the full SHA
    26ad6dd View commit details
    Browse the repository at this point in the history

  4. fix(doc/lean/library_style.org): remove unnecessary header line

    @avigad
    avigad committed May 16, 2015
    Configuration menu
    Copy the full SHA
    5ae63c0 View commit details
    Browse the repository at this point in the history

  5. fix(library/data/set/{classical_inverse.lean,map.lean}): protect defi… 

    …nitions in map, to avoid ambiguity
    @avigad
    avigad committed May 16, 2015
    Configuration menu
    Copy the full SHA
    63bb4b5 View commit details
    Browse the repository at this point in the history

  6. feat(library/algebra/group.lean): add coercions from additive (comm) … 

    …monoid to (comm) monoid
    @avigad
    avigad committed May 16, 2015
    Configuration menu
    Copy the full SHA
    87e4f7a View commit details
    Browse the repository at this point in the history

  7. refactor,feat(library/{data,algebra}): move bigops to algebra, define… 

    … sums
    @avigad
    avigad committed May 16, 2015
    Configuration menu
    Copy the full SHA
    eae047b View commit details
    Browse the repository at this point in the history

  8. feat(library/data/nat/bigops.lean): add finite products and sums for nat

    @avigad
    avigad committed May 16, 2015
    Configuration menu
    Copy the full SHA
    ff701a9 View commit details
    Browse the repository at this point in the history

Commits on May 17, 2015

  1. feat(library/data/default.lean): add rat and vector

    @avigad
    avigad committed May 17, 2015
    Configuration menu
    Copy the full SHA
    981bf93 View commit details
    Browse the repository at this point in the history

  2. feat(library/algebra/order): add alternate names for le.antisymm etc.

    @avigad
    avigad committed May 17, 2015
    Configuration menu
    Copy the full SHA
    7bde819 View commit details
    Browse the repository at this point in the history

  3. feat(library/init/nat.lean): add notation <= and >= for nat

    @avigad
    avigad committed May 17, 2015
    Configuration menu
    Copy the full SHA
    6dc1cfc View commit details
    Browse the repository at this point in the history

  4. refactor(library/algebra/group_bigops.lean,library/data/nat/bigops.le… 

    …an): simplify naming scheme for bigops
    @avigad
    avigad committed May 17, 2015
    Configuration menu
    Copy the full SHA
    4764f6e View commit details
    Browse the repository at this point in the history

  5. refactor(library/algebra/group_bigops.lean,library/data/nat/bigops.le… 

    …an): add ext principle, clean up file
    @avigad
    avigad committed May 17, 2015
    Configuration menu
    Copy the full SHA
    9720d84 View commit details
    Browse the repository at this point in the history

  6. feat(library/data/finset/basic.lean): add useful calculation rules fo… 

    …r quantifiers
    @avigad
    avigad committed May 17, 2015
    Configuration menu
    Copy the full SHA
    783dd61 View commit details
    Browse the repository at this point in the history

  7. feat(library/data/finset/bigops.lean): add Union for finsets

    @avigad
    avigad committed May 17, 2015
    Configuration menu
    Copy the full SHA
    6549940 View commit details
    Browse the repository at this point in the history

  8. feat(library/data/finset/card.lean): add card_Union_of_disjoint and o… 

    …ther theorems
    @avigad
    avigad committed May 17, 2015
    Configuration menu
    Copy the full SHA
    566acf4 View commit details
    Browse the repository at this point in the history

  9. feat(extras/latex/*): add listings style definition and instructions

    @avigad
    avigad committed May 17, 2015
    Configuration menu
    Copy the full SHA
    18742e8 View commit details
    Browse the repository at this point in the history