mathlib3
feat(tactic/local_cache): add tactic-block-local caching mechanism
#837

Merged

feat(tactic/local_cache): add tactic-block-local caching mechanism #837

cipher1024 merged 8 commits into master from local-cache

khoek force pushed from bb120606 to d603c900 6 years ago

cipher1024 requested a review from

robertylewis 6 years ago

cipher1024 requested a review from

digama0 6 years ago

cipher1024 assigned

cipher1024 6 years ago

cipher1024 commented on 2019-03-20

robertylewis commented on 2019-03-21

khoek force pushed from 8441adfd to 4fc7ea36 6 years ago

cipher1024 commented on 2019-04-02

feat(tactic/local_cache): add tactic-block-local caching mechanism

aa8715c7

fix(comment): improve comment for `mk_user_fresh_name`

9ba50afb

Better comment

2913092f

Much better tests + new `local_cache.get` function

88bbb39b

Big update, add cache scope parameter for tactic block or whole defin…

9d26fb6a

Tidy up

48fcd6af

Some docstrings + tidying + try to encapsulate a bit better

4baf81c5

Do apply_normed

ee9b450f

khoek force pushed from 79fea055 to ee9b450f 6 years ago

cipher1024 merged 13034ba3 into master 6 years ago

cipher1024 deleted the local-cache branch 6 years ago

Reviewers

cipher1024

robertylewis

digama0

Assignees

cipher1024

Labels

None yet

Milestone

No milestone