Agda.TypeChecking.Functions
etaExpandClause :: MonadTCM tcm => Clause -> tcm Clause Source #
Expand a clause to the maximal arity, by inserting variable patterns and applying the body to variables.
getDef :: Term -> TCM (Maybe QName) Source #
Get the name of defined symbol of the head normal form of a term. Returns Nothing if no such head exists.
Nothing