dad541265c
This PR moves many operations involving `String.Pos.Raw` to a the `String.Pos.Raw` namespace with the eventual aim of freeing up the `String` namespace to contain operations using `String.ValidPos` (to be renamed to `String.Pos`) instead. This PR adds the `String.ValidPos.set` and `String.ValidPos.modify` functions. After this PR, `String.pos_lt_eq` is no longer a `simp` lemma. Add `String.Pos.Raw.lt_iff` as a `simp` lemma if your proofs break. |
||
|---|---|---|
| .. | ||
| Add.lean | ||
| Extension.lean | ||
| Formatter.lean | ||
| Links.lean | ||
| Markdown.lean | ||
| Parser.lean | ||
| Syntax.lean | ||
| Types.lean | ||