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

Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Reflected

Documentation

type Args = [Arg Term] Source #

data Elim' a Source #

Constructors

Apply (Arg a) 
Instances
Unquote Elim Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Show a => Show (Elim' a) Source # 
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 Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

ToAbstract (Expr, Elim) Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type Elims = [Elim] Source #

data Abs a Source #

Constructors

Abs String a 
Instances
Show a => Show (Abs a) Source # 
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) Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM (Abs a) Source #

ToAbstract r a => ToAbstract (Abs r) (a, Name) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Methods

toAbstract :: Abs r -> WithNames (a, Name) Source #

type Type = Term Source #

data Sort Source #

Constructors

SetS Term 
LitS Integer 
UnknownS 
Instances
Show Sort Source # 
Instance details

Defined in Agda.Syntax.Reflected

Methods

showsPrec :: Int -> Sort -> ShowS #

show :: Sort -> String #

showList :: [Sort] -> ShowS #

Unquote Sort Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

ToAbstract Sort Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract