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

Safe HaskellNone

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 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.

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)