Agda-2.6.2.2: A dependently typed functional programming language and proof assistant

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.TypeChecking.Functions

Synopsis

- etaExpandClause :: MonadTCM tcm => Clause -> tcm Clause
- getDef :: Term -> TCM (Maybe QName)

# Documentation

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.