# Zulip Chat Archive

## Stream: new members

### Topic: Making a contribution to mathlib - lattice ordered groups

#### Christopher Hoskin (Aug 13 2021 at 19:46):

Hello, I'd like to offer a contribution to mathlib - a basic theory of lattice ordered groups: https://github.com/leanprover-community/mathlib/pull/8663

If this is of interest, please could I have write access to non-master branches of the mathlib repository? My GitHub username is mans0954.

Thank you,

Christopher Hoskin

#### Johan Commelin (Aug 13 2021 at 20:01):

https://github.com/leanprover-community/mathlib/invitations

#### Alex J. Best (Aug 13 2021 at 20:35):

@Christopher Hoskin once you've accepted the invite you can open a new version of that PR from a branch on mathlib and the CI will run on it.

#### Yury G. Kudryashov (Aug 13 2021 at 20:39):

Note that we have docs#covariant_class and docs#contravariant_class.

#### Alex J. Best (Aug 13 2021 at 20:53):

Some random thoughts from looking over the code, it looks pretty good overall!:

- You use
`simp`

in some places where it doesn't close the goal (pos_meet_neg_eq_zero), this is called a non-terminal simp and is generally discouraged as if the set of simp lemmas later changes (someone adds a new simplification perhaps) it can break your proof, its better in such situations to change simp to`squeeze_simp`

which will output a call to`simp only [...]`

instead that will be more robust. - In lemmas like
`join_eq_add_pos_sub`

the proof is a pure calc block, so doesn't need to be in a`begin... end`

just`:= calc ...`

will do. - Some of your very short proofs in tactic more are term mode one-liners, like
`lemma pos_sub_neg' (a : α) : a⁺ - a⁻ = a := (pos_sub_neg _).symm`

getting more experience with writing direct lean terms like this is always helpful to get rid of small goals faster. - if you have multiple rewrites in a row they can be combined like
`rw a, rw b,`

is equivalent to`rw [a, b]`

- are you aware of tactic#library_search? in
`abs_pos_eq`

where you write`-- I feel there ought to be a simpler way of finishing from here?`

putting instead`library_search`

tells me the proof can be finished with`exact nsmul_nonneg h 2,`

instead.

#### Patrick Massot (Aug 13 2021 at 21:04):

You should also read https://leanprover-community.github.io/contribute/style.html, especially the part about braces.

#### Christopher Hoskin (Aug 14 2021 at 07:59):

Thanks, I've created a branch within mathlib, but the CI is failing with the message "Error: ERR_RNT: Reserved notation outside tactic.reserved_notation" https://github.com/leanprover-community/mathlib/runs/3328082790

Having looked in reserved_notation it's not obvious to me what I've done wrong. Is there a way of seeing which line it's failing at?

Thanks.

#### Julian Berman (Aug 14 2021 at 08:03):

CI is hiding that for some reason (I have vague recollection there's desire to make that integrate better with the GitHub UI which is why that happened). Running it locally (by running `./scripts/lint-style.sh`

) it shows me:

```
:error file=src/algebra/lattice_ordered_group.lean,line=214,code=ERR_RNT::ERR_RNT: Reserved notation outside tactic.reserved_notation
::error file=src/algebra/lattice_ordered_group.lean,line=222,code=ERR_RNT::ERR_RNT: Reserved notation outside tactic.reserved_notation
```

#### Eric Wieser (Aug 14 2021 at 08:04):

The error message is also visible at https://github.com/leanprover-community/mathlib/compare/lattice_ordered_group

#### Eric Wieser (Aug 14 2021 at 08:04):

Where it is attached to the correct line number

Last updated: Dec 20 2023 at 11:08 UTC