Agda-2.5.2: A dependently typed functional programming language and proof assistant
Agda.Syntax.Reflected
type Args = [Arg Term] #
data Elim' a #
Constructors
Instances
Methods
unquote :: Term -> UnquoteM Elim #
showsPrec :: Int -> Elim' a -> ShowS #
show :: Elim' a -> String #
showList :: [Elim' a] -> ShowS #
toAbstract :: (Expr, Elims) -> WithNames Expr #
toAbstract :: (Expr, Elim) -> WithNames Expr #
type Elim = Elim' Term #
type Elims = [Elim] #
argsToElims :: Args -> Elims #
data Abs a #
showsPrec :: Int -> Abs a -> ShowS #
show :: Abs a -> String #
showList :: [Abs a] -> ShowS #
unquote :: Term -> UnquoteM (Abs a) #
toAbstract :: Abs r -> WithNames (a, Name) #
data Term #
showsPrec :: Int -> Term -> ShowS #
show :: Term -> String #
showList :: [Term] -> ShowS #
prettyTCM :: Term -> TCM Doc #
unquote :: Term -> UnquoteM Term #
toAbstract :: Term -> WithNames Expr #
toAbstract :: [Arg Term] -> WithNames [NamedArg Expr] #
type Type = Term #
data Sort #
showsPrec :: Int -> Sort -> ShowS #
show :: Sort -> String #
showList :: [Sort] -> ShowS #
unquote :: Term -> UnquoteM Sort #
toAbstract :: Sort -> WithNames Expr #
data Pattern #
showsPrec :: Int -> Pattern -> ShowS #
show :: Pattern -> String #
showList :: [Pattern] -> ShowS #
unquote :: Term -> UnquoteM Pattern #
toAbstract :: Pattern -> WithNames (Names, Pattern) #
data Clause #
showsPrec :: Int -> Clause -> ShowS #
show :: Clause -> String #
showList :: [Clause] -> ShowS #
unquote :: Term -> UnquoteM Clause #
toAbstract :: QNamed Clause -> WithNames Clause #
toAbstract :: [QNamed Clause] -> WithNames [Clause] #
data Definition #
showsPrec :: Int -> Definition -> ShowS #
show :: Definition -> String #
showList :: [Definition] -> ShowS #