leanprover-community/mathlib

Pull Requests Commits

Add misplaced test case for simplify_equations

JLimperg committed 5 years ago

e5ca62f2

Inline and remove replace' utility function

JLimperg committed 5 years ago

b65505ae

Remove unused utility function

JLimperg committed 5 years ago

22031137

Restructure and document unify_equations

JLimperg committed 5 years ago

8a10319d

Implement unify_constructor_headed via injection

JLimperg committed 5 years ago

537d3eb6

Move utilities and equation unification into separate files

JLimperg committed 5 years ago

dd142a8f

Remove some utility functions

JLimperg committed 5 years ago

576b90d8

Format everything according to mathlib style

JLimperg committed 5 years ago

58a0a85c

Minor improvements

JLimperg committed 5 years ago

d1d15918

Make index eq simplification work with nested datatypes

JLimperg committed 5 years ago

0855e715

Make sure that cases' can eliminate false

JLimperg committed 5 years ago

be38e74f

Add TODO about new injection

JLimperg committed 5 years ago

a4e96b1a

Avoid normalisation in simplify_index_equations

JLimperg committed 5 years ago

a54bb8a0

Clean up imports

JLimperg committed 5 years ago

7f03c8cf

Add lots of test cases from LoVe

JLimperg committed 5 years ago

4712c116

Minor refactoring of generalize_complex_index_args

JLimperg committed 5 years ago

b472cd21

Avoid injection tactic

JLimperg committed 5 years ago

a24851a7

Fix index generalisation and structure value replacement

JLimperg committed 5 years ago

aa211f97

Import tactic.core instead of tactic.basic

JLimperg committed 5 years ago

26f27846

Add basic tracing

JLimperg committed 5 years ago

0f86b2c2

Remove dependency on linarith

JLimperg committed 5 years ago

a13a448a

Fix bugs related to index and auto-generalisation

JLimperg committed 5 years ago

700f186e

Cosmetics in tests

JLimperg committed 5 years ago

4968af5a

Fix index eq simplification for non-normal equations

JLimperg committed 5 years ago

d65fd0e7

Fix index generalisation generalising too much

JLimperg committed 5 years ago

3f68039f

JLimperg committed 5 years ago

dfa10002

Add support for `fixing *` and `generalizing`

JLimperg committed 5 years ago

1162ab68

Generalise mmap_with_index'

JLimperg committed 5 years ago

6aff398b

Change default name of constructor args in Prop

JLimperg committed 5 years ago

6a0c7bd2

Simplify simplify_index_equation

JLimperg committed 5 years ago

dc1d641d

Newer Older