remove comments on orientation def

[JamesGallicchio]

No description provided.

[digama0]

why?

[JamesGallicchio]

Reviewer 1 said that the comments were confusingly formatted (didn't realize they were comments at first) and unhelpful. I was going to just reformat it as

inductive Orientation
| cw        -- clockwise, det < 0
| ccw       -- counter clockwise, det > 0
| collinear

to clarify that they are comments, but I still find it not particularly helpful for readers?

[bsubercaseaux]

mmmh, I think:

1. Inline (as you did) seems to look better)
2. one option is to add a footnote saying that's how Lean comments look like
3. another option is to remove the comments altogether.

Either is fine with me!

[digama0]

I think it's best to keep the comments, since it may not be obvious that cw is referring to clockwise, and also its relationship to positivity is important for things like ofReal. You could also make them doc-comments and beef them up to proper sentences or at least sentence fragments though.

[JamesGallicchio]

I think for the paper the positivity element is not so important, but I left intuitive comments for explanation.

I added doc comments to the actual codebase since that seems like a good idea.