Commit history

1. Commits on Jul 20, 2018

   • feat(tactic/h_generalize): remove `cast` expressions from goal (#198)

     

     cipher1024

     authored and

     digama0

     committed
     23a5591View commit details

     Copy full SHA for 23a5591

     View code at this pointBrowse repository at this point
2. Commits on Jul 19, 2018

   • fix(tactic/refine_struct): fix support for source structures

     

     cipher1024

     authored and

     digama0

     committed
     c2f54adView commit details

     Copy full SHA for c2f54ad

     View code at this pointBrowse repository at this point
3. Commits on Jul 16, 2018

   • feat(tactic/interactive): add apply_rules tactic (#190)

     

     sgouezel

     authored and

     digama0

     committed
     4c6d7e2View commit details

     Copy full SHA for 4c6d7e2

     View code at this pointBrowse repository at this point

   • feat(tactic/tauto): improve coverage and performances of tauto (#180)

     

     cipher1024

     authored and

     digama0

     committed
     b0de694View commit details

     Copy full SHA for b0de694

     View code at this pointBrowse repository at this point

   • feat(category/applicative): `id` and `comp` functors; proofs by `norm` (#184)

     

     cipher1024

     authored and

     johoelzl

     committed
     844c665View commit details

     Copy full SHA for 844c665

     View code at this pointBrowse repository at this point
4. Commits on Jul 6, 2018

   • feat(tactic/cache): split cache related tactics off from `tactic.interactive`

     

     cipher1024

     authored and

     digama0

     committed
     28e011dView commit details

     Copy full SHA for 28e011d

     View code at this pointBrowse repository at this point

   • feat(tactic/tauto): handle `or` in goal

     

     cipher1024

     authored and

     digama0

     committed
     06f4778View commit details

     Copy full SHA for 06f4778

     View code at this pointBrowse repository at this point
5. Commits on Jul 4, 2018

   • feat(tactic/tauto): consider `true` and `false`

     

     cipher1024

     authored and

     digama0

     committed
     a784602View commit details

     Copy full SHA for a784602

     View code at this pointBrowse repository at this point
6. Commits on Jun 25, 2018

   • feat(tactic/solve_by_elim): writing a symm_apply tactic for solve_by_elim (#164)

     Show description for 90aeb8e
     

     kim-em

     authored and

     digama0

     committed
     90aeb8eView commit details

     Copy full SHA for 90aeb8e

     View code at this pointBrowse repository at this point
7. Commits on Jun 21, 2018

   • feat(tactic/refine_struct): match `{ .. }` in subexpressions (#162)

     

     cipher1024

     authored and

     digama0

     committed
     4082136View commit details

     Copy full SHA for 4082136

     View code at this pointBrowse repository at this point
8. Commits on Jun 19, 2018

   • feat(tactic/ext): `ext` now applies to `prod`; fix `ext` on function types (#158)

     

     cipher1024

     authored and

     digama0

     committed
     0a0e8a5View commit details

     Copy full SHA for 0a0e8a5

     View code at this pointBrowse repository at this point

   • feat(split_ifs): fail if no progress (#153)

     

     kim-em

     authored and

     digama0

     committed
     8609a3dView commit details

     Copy full SHA for 8609a3d

     View code at this pointBrowse repository at this point
9. Commits on May 28, 2018

   • fix(tactics/wlog): allow union instead of disjunction; assume disjunction in strict associcated order; fix discharger

     johoelzl

     committed
     0022068View commit details

     Copy full SHA for 0022068

     View code at this pointBrowse repository at this point
10. Commits on May 23, 2018

    • feat(tactic/split_ifs): add if-splitter

      

      gebner

      authored and

      johoelzl

      committed
      509934fView commit details

      Copy full SHA for 509934f

      View code at this pointBrowse repository at this point
11. Commits on May 20, 2018

    • fix(tactic/interactive): make rcases handle nested constructors correctly

      Show description for 741469a
      

      rwbarton

      authored and

      digama0

      committed
      741469aView commit details

      Copy full SHA for 741469a

      View code at this pointBrowse repository at this point
12. Commits on May 16, 2018

    • feat(tactic): generalize wlog to support multiple variables and cases, allow to provide case rule

      johoelzl

      committed
      d8c33e8View commit details

      Copy full SHA for d8c33e8

      View code at this pointBrowse repository at this point
13. Commits on May 10, 2018

    • feat(data/multiset): add relator

      johoelzl

      committed
      62833caView commit details

      Copy full SHA for 62833ca

      View code at this pointBrowse repository at this point
14. Commits on May 4, 2018

    • feat(tactic/mk_iff_of_inductive_prop): add tactic to represent inductives using logical connectives

      johoelzl

      committed
      e4c64fdView commit details

      Copy full SHA for e4c64fd

      View code at this pointBrowse repository at this point
15. Commits on Apr 25, 2018

    • feat(tactic/interactive): add `clean` tactic

      Show description for 44271cf
      digama0

      committed
      44271cfView commit details

      Copy full SHA for 44271cf

      View code at this pointBrowse repository at this point

    • feat(tactic/generalize_hyp): a version of `generalize` that also applies to assumptions (#110)

      

      cipher1024

      authored and

      digama0

      committed
      e4e4659View commit details

      Copy full SHA for e4e4659

      View code at this pointBrowse repository at this point
16. Commits on Apr 24, 2018

    • feat(tactic/convert): tactic similar to `refine` (#116)

      Show description for 3b73ea1
      

      cipher1024

      authored and

      digama0

      committed
      3b73ea1View commit details

      Copy full SHA for 3b73ea1

      View code at this pointBrowse repository at this point

    • feat(tactic/ext): new `ext` tactic and corresponding `extensionality` attribute

      

      cipher1024

      authored and

      digama0

      committed
      e2c7421View commit details

      Copy full SHA for e2c7421

      View code at this pointBrowse repository at this point

    • fix(tactic/wlog): in the proof of completeness, useful assumptions were not visible

      

      cipher1024

      authored and

      digama0

      committed
      d862939View commit details

      Copy full SHA for d862939

      View code at this pointBrowse repository at this point
17. Commits on Apr 16, 2018

    • chore(*): trailing spaces

      digama0

      committed
      d5c73c0View commit details

      Copy full SHA for d5c73c0

      View code at this pointBrowse repository at this point
18. Commits on Apr 5, 2018

    • fix(*): finish lean update

      digama0

      committed
      c87f1e6View commit details

      Copy full SHA for c87f1e6

      View code at this pointBrowse repository at this point
19. Commits on Apr 4, 2018

    • fix(*): update to lean

      Show description for 5717986
      digama0

      committed
      5717986View commit details

      Copy full SHA for 5717986

      View code at this pointBrowse repository at this point
20. Commits on Mar 21, 2018

    • fix(test suite): remove `sorry` warning in test suite

      

      cipher1024

      authored and

      digama0

      committed
      486e4edView commit details

      Copy full SHA for 486e4ed

      View code at this pointBrowse repository at this point
21. Commits on Mar 8, 2018

    • feat(tactic): add `wlog` (without loss of generality), `tauto`, `auto` and `xassumption`

      Show description for a7d8c5f
      

      cipher1024

      authored and

      johoelzl

      committed
      a7d8c5fView commit details

      Copy full SHA for a7d8c5f

      View code at this pointBrowse repository at this point
22. Commits on Dec 11, 2017

    • chore(tests/finish3): rename definition with same name

      

      gebner

      authored and

      digama0

      committed
      6b10d8dView commit details

      Copy full SHA for 6b10d8d

      View code at this pointBrowse repository at this point
23. Commits on Dec 6, 2017

    • chore(.): adapt to change bc89ebc19c93392419b7bab8b68271db12855dc5 (improve how induction hypotheses are named)

      

      spl

      authored and

      digama0

      committed
      fd803b6View commit details

      Copy full SHA for fd803b6

      View code at this pointBrowse repository at this point
24. Commits on Dec 5, 2017

    • chore(.): adapt to change 6d96741010f5f36f2f4f046e4b2b8276eb2b04d4 (provide names for constructor arguments)

      johoelzl

      committed
      8273536View commit details

      Copy full SHA for 8273536

      View code at this pointBrowse repository at this point

    • chore(.): adapt to change b7322e28c12d274ccec992b7fc49d35b2e56a2a4 (remove AC simp rules)

      johoelzl

      committed
      f6474f0View commit details

      Copy full SHA for f6474f0

      View code at this pointBrowse repository at this point

    • feat(tactic/norm_num): add support for {nat,int}.div

      digama0

      committed
      8d27f70View commit details

      Copy full SHA for 8d27f70

      View code at this pointBrowse repository at this point
25. Commits on Nov 24, 2017

    • feat(data/set/finite): unify fintype and finite developments

      Show description for 2c84af1
      digama0

      committed
      2c84af1View commit details

      Copy full SHA for 2c84af1

      View code at this pointBrowse repository at this point

    • feat(algebra/group_power): remove overloaded ^ notation, add smul

      digama0

      committed
      c03c16dView commit details

      Copy full SHA for c03c16d

      View code at this pointBrowse repository at this point