Mario Carneiro
Mario Carneiro
- [x] Depends on: #735 - [x] Depends on: #737 - [x] Depends on: #738 This adds RBMap lemmas corresponding to all of the RBSet lemmas.
Based on discussions on [Zulip](https://leanprover.zulipchat.com/#narrow/stream/348111-std4/topic/Porting.20just.20functionality/near/354657447). Still needs more love to make it polished.
This was a surprisingly challenging proof. It really highlights some of the pain involved in verifying programs which perform many array modifications without something isomorphic to separation logic, because one...
- [x] Depends on: #735 - [x] Depends on: #737 - [x] Depends on: #738 - [x] Depends on: #739 - [x] Depends on: #740 Continuation of the RBMap series....
Complement to #762. Adds List version of all the definitions in `Data.Array.Merge`. Also adds `List.mergeSort` (upstreamed from mathlib), as a replacement for `Array.qsort` on lists (because `qsort` cannot easily be...
To ease new contributions, we should write down the style rules (indentation, usage of trailing punctuation and structuring tactics) so that we have a place to point contributors to. Currently...
The `@[simp]` attribute is used by both simp and dsimp, so it is possible for a rfl lemma to have a proof by simp but not one by dsimp, and...
Related to #47. example : true := sorry example : true := sorry ... example : true := sorry #print nat There are 250 lines of `example : true` there....
```lean include h omit h ``` These lean 3 commands can be used to change inclusion behavior of variables, and there is currently no lean 4 analogue.
```lean reserve infix `foo`:20 precedence `bar`:20 ``` These are rarely used and can probably be ignored.