Allow pattern-matching in variable definitions

[lukaszcz]

• Closes Allow pattern-matching in lets (and other definitions) for records and other single-constructor types #3118
• Allows patterns on the left-hand sides of definitions. To avoid clashes with constructor names, the patterns need to be enclosed in parentheses or have the form n@.... A standalone symbol x in a definition x := ... is always interpreted as an identifier even if there exists a constructor x.
• Left-hand side patterns are desugared in the translation from Concrete to Internal. If the inductive type has more than one constructor, non-exhaustive pattern matching error will later be given by the pattern matching compiler.

[janmasrovira]

reviewing...