Mathlib Changelog
Changelog
About
Github
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