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