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

Safe Haskell | Safe-Infered

Agda.TypeChecking.DisplayForm

# Documentation

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

matchDisplayForm :: DisplayForm -> Args -> Maybe DisplayTerm

class Match a where

Methods

match :: Nat -> a -> a -> Maybe [Term]

Instances

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