leanprover-community/mathlib

Pull Requests Commits

Remove local_names_option

JLimperg committed 5 years ago

d33341c9

Replace rb_multimap with core's rb_lmap

JLimperg committed 5 years ago

e60e352c

Synchronise with latest version of unify_equations branch

JLimperg committed 5 years ago

5265d307

Minor changes to some utility functions

JLimperg committed 5 years ago

6a50f1d0

Refactor tactics for decomposing applications

JLimperg committed 5 years ago

ded11fd2

Fix test breakage due to upstream changes

JLimperg committed 5 years ago

c288ba81

Remove some unused instance args

JLimperg committed 5 years ago

2d4bfa6b

Refactor simplify_ih and related functions

JLimperg committed 5 years ago

37bbbeb4

Minor refactoring of constructor_renames

JLimperg committed 5 years ago

ffb2ffd4

Remove/update some TODO comments

JLimperg committed 5 years ago

a7383928

Remove unused utility functions

JLimperg committed 5 years ago

a1628b9d

Move some util functions to default.lean

JLimperg committed 5 years ago

6e0c72bd

Remove some outdated TODOs

JLimperg committed 5 years ago

19db9cc3

Better docs for 'Prop' constructor arg naming rule

JLimperg committed 5 years ago

9fe2fcaa

Change error reporting of constructor arg naming rules

JLimperg committed 5 years ago

1d0ed468

type_based_naming: fix universe level of variable_names

JLimperg committed 5 years ago

f8d42dc3

Add hint about tracing to docs

JLimperg committed 5 years ago

a15180b6

Move tactic.type_based_naming to tactic.induction.type_based_naming

JLimperg committed 5 years ago

bd69b63a

Move induction.lean to induction/default.lean

JLimperg committed 5 years ago

aadf7c35

Move a utility function to util

JLimperg committed 5 years ago

6d834224

Remove structure index simplification

JLimperg committed 5 years ago

b91b0a74

Move some functions to util; add lots of docs

JLimperg committed 5 years ago

c2b60106

Add another test case for constructor naming

JLimperg committed 5 years ago

30faebd0

unify_equations: fix a bug with generalised inductive types

JLimperg committed 5 years ago

151dcf11

Update to latest mathlib master

JLimperg committed 5 years ago

c2f5bbcd

unify_equations: remove trivial hyps generated by injection_with

JLimperg committed 5 years ago

171006b7

Minor test improvements

JLimperg committed 5 years ago

de1074b4

Add a less synthetic test case for auto-generalisation

JLimperg committed 5 years ago

e734856a

Some doc improvements

JLimperg committed 5 years ago

ba13ee35

Remove name_set and rb_set unioning utility functions

JLimperg committed 5 years ago

2924a0e4

Older