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

Safe Haskell | None

Agda.TypeChecking.DisplayForm

# Documentation

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

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

class Match a where

Methods

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

Instances

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