Safe Haskell | None |
---|
Agda.TypeChecking.DisplayForm
- displayForm :: QName -> Args -> TCM (Maybe DisplayTerm)
- matchDisplayForm :: DisplayForm -> Args -> MaybeT TCM DisplayTerm
- class Match a where
Documentation
displayForm :: QName -> Args -> TCM (Maybe DisplayTerm)Source
Find a matching display form for q vs
.
In essence this tries to reqwrite q vs
with any
display form q ps --> dt
and returns the instantiated
dt
if successful. First match wins.
matchDisplayForm :: DisplayForm -> Args -> MaybeT TCM DisplayTermSource
Match a DisplayForm
q ps = v
against q vs
.
Return the DisplayTerm
v[us]
if the match was successful,
i.e., vs / ps = Just us
.