Application package:Agda
Parse a list of expressions (typically from a
RawApp) into an
application.
If a clause is over-applied we can't trust the head (Issue 2944). For
instance, the clause might be `f ps = u , v` and the actual call `f vs
.fst`. In this case the head will be the head of u rather
than `_,_`.
Expected an argument of the form f e1 e2 .. en.
The target of a constructor isn't an application of its datatype. The
Type records what it does target.
A function is applied to a hidden argument where a non-hidden was
expected.
checkApplication hd args e t checks an application.
Precondition:
Application hs args = appView e
checkApplication disambiguates constructors (and continues to
checkConstructorApplication) and resolves pattern synonyms.
Precondition: Application hd args = appView e.
Check an application of a section.