Meta level data

[SkySkimmer]

This pull request introduces:

• a new variant of values, called tags, consisting of a quoted identifier (eg 'foo) applied to a list of arbitrary values. For instance:

  'closure_with_judgement (fun x -> x) Type
  

• a match statement

  match v with
    | [pattvars] pattern => comp
    ...
    end
  

  where pattvars is a list of variables to be instantiated by values on a match.
  The patterns are not linear. Terms are compared modulo alpha equality, and term judgements are compared through the terms only.
  If the name of a binder is a pattern variable (eg x in λ [x] foo), that variable will be instantiated with the corresponding atom.
  The value matching a sub-pattern can be used to instantiate a variable with the as keyword, eg

   | [x y] 'cons _ (('cons x _) as y)
  

  will match list-like tag values with at least 2 elements, instantiating x with the second element and y with the tail.

See upcoming tests for examples.