lean icon indicating copy to clipboard operation
lean copied to clipboard

feat(init/data/cached): Caching mechanism [WIP]

Open digama0 opened this issue 6 years ago • 0 comments

Back from the dead (https://github.com/leanprover/lean/pull/1628). @cipher1024 @EdAyers There were some worrisome review comments about ts_clone that I don't think I addressed before the PR was closed. I'll take another look at it but if either of you know what needs to be done I'd appreciate it.

I'm thinking of renaming cached to mutable and eliminating the inhabited argument. Originally I was considering the idea of using cached cells for memory reclamation on running programs, but I think we're going a different direction with this and so it doesn't make that much sense anymore.

digama0 avatar May 10 '19 00:05 digama0