Expand description
What moved between two checkpoints, as a fact rather than as a patch.
The part crates/kernel/spec/Change.lean specifies this module.
Here rather than beside the git call that produces it, for the reason
Restoration is here: three places need this shape — storage reads
it off two trees, wire carries it, and the interface draws it —
and wire cannot see storage. Defining it twice and converting
between the copies would be two definitions of what a file change is,
and the one that drifts is always the one nobody is looking at.
Paths and counts only. Patch text is file content, and file content
leaving this machine is the question secret::scan exists to answer;
a hunk therefore has to be asked for on its own and scanned like
anything else, which is why no field here can hold one.
Structs§
- File
Change - One file, as the difference between two trees describes it.