| Safe Haskell | Safe-Inferred |
|---|---|
| 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.