Skip to content

Commit

Permalink
fix(docs/style): precise a style rule and fixes a github markdown iss…
Browse files Browse the repository at this point in the history
…ue (#290)
  • Loading branch information
PatrickMassot authored and johoelzl committed Aug 29, 2018
1 parent bab3813 commit 49fb2db
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions docs/style.md
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,7 @@ open nat eq.ops

### Structuring definitions and theorems ###

Use spaces around ":" and ":=". Put them before a line break rather
Use spaces around ":", ":=" or infix operators. Put them before a line break rather
than at the beginning of the next line.

Use two spaces to indent. You can use an extra indent when a long line
Expand Down Expand Up @@ -253,7 +253,7 @@ theorem reverse_reverse : ∀ (l : list α), reverse (reverse l) = l
```


### Tactic mode ###
### Tactic mode ###

When opening a tactic block, `begin` is not indented but everything
inside is indented, as in:
Expand Down

0 comments on commit 49fb2db

Please sign in to comment.