lean
lean copied to clipboard
feat(init/data/cached): Caching mechanism [WIP]
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.