Add insert and take methods for PointsToRaw (inplace join/split)

verus-lang / verus

Verified Rust for low-level systems code

MIT License

1.15k stars 66 forks source link

Add insert and take methods for PointsToRaw (inplace join/split) #1117

Closed ouuan closed 4 months ago

ouuan commented 4 months ago

Added in-place versions of join/split functions for PointsToRaw.

Note: The implementation (proof) is what I am currently doing in my own project. I'm not sure if there is a better implementation or even one that makes this PR redundant.