search

mikeshulman / Coq-HoTT

Homotopy type theory
http://homotopytypetheory.org/
Other
12 stars 4 forks source link

some style changes #14

Closed Alizter closed 4 years ago

Alizter commented 4 years ago

Here are some style changes.

I've reformatted records, classes so that ; always comes at the end of a line like a period. I've reduced some of the indentation and spaces things out so they are easier to see.

I've removed the maximal insertion of implicit to minimally inserted. You could see issues when trying to show that opyon is a functor. Coq can now guess this automatically without wrongly assuming the categories.

I've also reduced some indentation in the definitions.

You don't have to like all my changes, but I am happy to keep only the ones you want.

Alizter commented 4 years ago

I've submitted this as a PR so we can talk about the changes. I also would prefer merging this tomorrow with everybody present so that we don't confuse anyone.