Agda-2.6.4.1: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.TypeChecking.DisplayForm

Description

Tools for DisplayTerm and DisplayForm.

Synopsis

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.