Safe Haskell	None

Agda.TypeChecking.DisplayForm

Synopsis

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 DisplayTerm Source

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.

class Match a whereSource

Methods

match :: a -> a -> MaybeT TCM [Term]Source

Instances

Match Level
Match Sort
Match Term
Match a => Match [a]
Match a => Match (Elim' a)
Match a => Match (Arg a)