Document alternative type declaration syntax

[jpetkau]

In the introduction to syntax for declaring data types, document the ability to declare types via constructor signatures in addition to the Haskell-like syntax.

This syntax seems to be documented nowhere (not even in the book), and is just used without explanation when introducing dependent types like Fin that require it. From personal experience, this is extremely confusing to newcomers to Idris.

(I'm not sure if this is the best place to document it, but it needs to be somewhere where it will be easily found, and this is what comes up for a Google search for "idris data types".)

[LeifW]

Thanks for the contribution - and sorry this didn't get attention earlier. You're right - that syntax can be confusing when first encountering it - and I think examples showing the same data type defined both ways are helpful for those coming from e.g. Haskell. Perhaps a mention of it being called GADT (in Haskell) or Agda syntax would be helpful, as in "The second, more general kind of data type, is defined using Agda or GADT style syntax. " - http://docs.idris-lang.org/en/latest/reference/syntax-guide.html#data-types

[LeifW]

Or maybe just a link to the reference from the tutorial? I think examples showing the same data type defined both ways would be helpful in the reference - not just showing things snipped from the existing library. The current examples in the reference are useful for showing the why of GADTs, but not as much the how, i.e. how that "new" syntax maps to syntax they may already be familiar with.

[jfdm]

Apologies that this has sat for a while.

These changes should be merged ASAP, they are important for making things clearer.

I think improving them with reference to 'GADT/Agda' style forms can come later.

[jfdm]

If there are no objections from @jpetkau then I will merge tomorrow.

[jfdm]

@jpetkau Thanks! I've merged this now.

If anyone wants to implement the recommended improvements suggested by @LeifW then please go ahead.