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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.DisplayForm

Description

Tools for `DisplayTerm` and `DisplayForm`.

Synopsis

- displayForm :: MonadDisplayForm m => QName -> Elims -> m (Maybe DisplayTerm)

# Documentation

displayForm :: MonadDisplayForm m => QName -> Elims -> m (Maybe DisplayTerm) Source #

Find a matching display form for `q es`. In essence this tries to rewrite `q es` with any display form `q ps --> dt` and returns the instantiated `dt` if successful. First match wins.