Ali Caglayan

@mikeshulman What to do then? :-)

I feel like if rapply were smart enough to look at the goal and guess immediately how many holes are needed, a lot of these problems wouldn't occur. @JasonGross didn't...

@JasonGross OK, I guess I was confusing it with the unspecified number of holes version then?

Don't we have a tactic `constructor` that does this? I only found out last week.

I think we will only rename the type `nat` to `Nat` whilst the lemmas `nat_X` will stay as they are since they are following convention.

Is this still possible? I would be in favour of something like this.

Would it be sensible to use `x^` for inverses, since it is more economical to type. We can probably set this up without affecting our notation for paths.

Once my torus PR #1066 is merged, I have a PR that will reorganise the Pointed file into a library. I will see, after that is merged, if making pMap...

So it is not as easy as setting pMap to be a type. I have tried the following: ``` (** ** Pointed functions *) (* A pointed map is a...

@mikeshulman If I understand coercions correctly, then pMap is being coerced into Funclass. I am not so sure about IsPointed in general however. When I was defining homotopy groups, I...