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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Rules.Display

Synopsis

- checkDisplayPragma :: QName -> [NamedArg Pattern] -> Expr -> TCM ()

# Documentation

checkDisplayPragma :: QName -> [NamedArg Pattern] -> Expr -> TCM () Source #

Add display pragma if well-formed. Otherwise, throw `InvalidDisplayForm` warning and ignore it.