Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-04-02 11:22 13034ba3

View on Github →

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

Estimated changes

Modified src/meta/expr.lean

added def name.from_components

Modified src/tactic/basic.lean

Created src/tactic/local_cache.lean

added def tactic.local_cache.internal.def_local.FNV_OFFSET_BASIS

added def tactic.local_cache.internal.def_local.FNV_PRIME

added def tactic.local_cache.internal.def_local.RADIX

added def tactic.local_cache.internal.def_local.hash_byte

added def tactic.local_cache.internal.def_local.hash_string

Created test/local_cache.lean

added def block_local.TEST_NS_1

added def block_local.TEST_NS_2

added structure block_local.dummy

added def block_local.my_def_1

added def block_local.my_def_2

added def block_local.my_definition'

added def block_local.my_definition

added theorem block_local.my_lemma'

added theorem block_local.my_lemma

added theorem block_local.my_lemma_1

added theorem block_local.my_lemma_2

added theorem block_local.my_lemma_3

added theorem block_local.my_test_ns

added theorem block_local.my_test_ps

added def collision.TEST_NS

added theorem collision.my_lemma_1

added theorem collision.my_lemma_2

added theorem collision.my_lemma_3

added theorem collision.my_lemma_4

added def def_local.TEST_NS_1

added def def_local.TEST_NS_2

added structure def_local.dummy

added def def_local.my_def_1

added def def_local.my_def_2

added def def_local.my_definition'

added def def_local.my_definition

added theorem def_local.my_lemma'

added theorem def_local.my_lemma

added theorem def_local.my_lemma_1

added theorem def_local.my_lemma_2

added theorem def_local.my_lemma_3

added theorem def_local.my_test_ns

added theorem def_local.my_test_ps