| demand(final-result(krate)): | |
| demand(partioning(krate)) | |
| for each cgu in partioning: | |
| demand(object_code(cgu)) | |
| demand(partioning(krate)): | |
| compute and return map with all partitions, a whole-krate process | |
| demand(partioning(cgu)): | |
| let partioning = demand(partioning(krate)) |
| Had a good chat with aturon about chalk. The key outcome was the realization | |
| that the basic structure of our prover is: | |
| Solve(Env, Goal) = LifetimeGoal | |
| is meant to imply that (in logical) | |
| Env, LifetimeGoal |- Goal | |
| This should always be achievable, since in the limit we can make |
non-lexical lifetimes
plan exists to address
nested method calls
vec.push(vec.len()