leanprover/LNSym

memory: add zero byte read/write theorems

Closed this issue · 1 comments

bollu commented

See #90 (comment) for context.

bollu commented

This is addressed, and we have the theorems read_bytes_zero_eq and write_bytes_zero