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

Safe HaskellNone

Agda.TypeChecking.DisplayForm

Documentation

displayForm :: QName -> Args -> TCM (Maybe DisplayTerm)Source

matchDisplayForm :: DisplayForm -> Args -> TCM (Maybe DisplayTerm)Source

class Match a whereSource

Methods

match :: Nat -> a -> a -> TCM (Maybe [Term])Source

Instances

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