Support Absurd Patterns

[CodaFi]

Sema is aware of absurd patterns, which allow one to omit the body of a function when pattern clauses cause contradictions.

proj : forall {n : N} {X : Type} → Vec X n → Fin n → X
proj [] ()
proj (cons x xs) zero = x
proj (cons x xs) (suc i) = proj xs i

The syntax for this needs to be added to the grammar and to the parser. Scope check need not concern itself with whether performing an inversion on the parameter will introduce a contradiction, it just needs to lower down to an empty Clause.Body.