Application package:Agda
Expected a type to be an application of a particular datatype.
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.
Parse a list of expressions (typically from a
RawApp) into an
application.
Parse an expression into a module application (an identifier plus a
list of arguments).
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 `_,_`.
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.