Commit 2021-02-10 00:03 18b378d8
View on Github →chore(data/fin): reorder file to group declarations (#6109)
The data/fin
file has a lot of definitions and lemmas. This reordering groups declarations and places ones that do not rely on fin
operations first, like order. No definitions or lemma statements have been changed. A minimal amount of proofs have been rephrased. No reformatting of style has been done. Section titles have been added.
This is useful in preparation for redefining fin
operations (lean#527). Additionally, it allows for better organization for other refactors like making pred
and pred_above
total.