Safe Haskell	None
Language	Haskell2010

Agda.Syntax.Reflected

Documentation

data Elim' a #

Constructors

Instances

Unquote Elim #
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM Elim #
Show a => Show (Elim' a) #
Instance details Defined in Agda.Syntax.Reflected Methods showsPrec :: Int -> Elim' a -> ShowS # show :: Elim' a -> String # showList :: [Elim' a] -> ShowS #
ToAbstract (Expr, Elims) Expr #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: (Expr, Elims) -> WithNames Expr #
ToAbstract (Expr, Elim) Expr #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: (Expr, Elim) -> WithNames Expr #

type Elims = [Elim] #

data Abs a #

Constructors

Instances

Show a => Show (Abs a) #
Instance details Defined in Agda.Syntax.Reflected Methods showsPrec :: Int -> Abs a -> ShowS # show :: Abs a -> String # showList :: [Abs a] -> ShowS #
Unquote a => Unquote (Abs a) #
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM (Abs a) #
ToAbstract r a => ToAbstract (Abs r) (a, Name) #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: Abs r -> WithNames (a, Name) #

data Term #

Constructors

Instances

Show Term #
Instance details Defined in Agda.Syntax.Reflected Methods showsPrec :: Int -> Term -> ShowS # show :: Term -> String # showList :: [Term] -> ShowS #
PrettyTCM Term #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Term -> TCM Doc #
Unquote Term #
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term0 -> UnquoteM Term #
Unquote Elim #
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM Elim #
ToAbstract Term Expr #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: Term -> WithNames Expr #
ToAbstract [Arg Term] [NamedArg Expr] #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: [Arg Term] -> WithNames [NamedArg Expr] #
ToAbstract (Expr, Elims) Expr #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: (Expr, Elims) -> WithNames Expr #
ToAbstract (Expr, Elim) Expr #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: (Expr, Elim) -> WithNames Expr #

data Sort #

Constructors

Instances

Show Sort #
Instance details Defined in Agda.Syntax.Reflected Methods showsPrec :: Int -> Sort -> ShowS # show :: Sort -> String # showList :: [Sort] -> ShowS #
Unquote Sort #
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM Sort #
ToAbstract Sort Expr #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: Sort -> WithNames Expr #

Constructors

Instances

Show Pattern #
Instance details Defined in Agda.Syntax.Reflected Methods showsPrec :: Int -> Pattern -> ShowS # show :: Pattern -> String # showList :: [Pattern] -> ShowS #
Unquote Pattern #
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM Pattern #
ToAbstract Pattern (Names, Pattern) #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: Pattern0 -> WithNames (Names, Pattern) #

Constructors

Clause [Arg Pattern] Term
AbsurdClause [Arg Pattern]

Instances

Show Clause #
Instance details Defined in Agda.Syntax.Reflected Methods showsPrec :: Int -> Clause -> ShowS # show :: Clause -> String # showList :: [Clause] -> ShowS #
Unquote Clause #
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM Clause #
ToAbstract (QNamed Clause) Clause #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: QNamed Clause0 -> WithNames Clause #
ToAbstract [QNamed Clause] [Clause] #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: [QNamed Clause0] -> WithNames [Clause] #

Constructors

Instances

Show Definition #
Instance details Defined in Agda.Syntax.Reflected Methods showsPrec :: Int -> Definition -> ShowS # show :: Definition -> String # showList :: [Definition] -> ShowS #