Remove the syntactical construct of parameter groups

[fmease]

For future reference, the snippet constant '(A B: Type) (a: A) (_: B): A = a is – at the time of this writing – syntactic sugar for constant '(A: Type) '(B: Type) (a: A) (_: B): A = a. In general, any (a0 a1 … an), '(a0 a1 … an: T) etc. after the binder of a value, data or constructor declaration expands to a0 a1 … an, '(a0: T) '(a1: T) … '(an: T), etc. respectively.

The motivation for this feature is not having that much boilerplate around implicit (!) type (!) parameters:

;; e.g:
compose '(A B C: Type) (f: A -> B) (g: B -> C): A -> C = \a => g (f a)
;; instead of:
compose '(A: Type) '(B: Type) '(C: Type) (f: A -> B) (g: B -> C): A -> C = \a => g (f a)

However, the actual origin of this verbosity is the requirement – existing at the time of this writing – that parameters of declarations (inside of namespaces) have to be type-annotated.

With the implementation of #102, though, the actual underlying issue would be fixed. Observe how much shorter the code would look:

compose 'A 'B 'C (f: A -> B) (g: B -> C): A -> C = \a => g (f a)

[fmease]

Fixed in 18e4e8e2cb68c8b93d2c41ef84004b0dc0dd8d59.