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

Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Reflected

Documentation

type Args = [Arg Term] #

data Elim' a #

Constructors

Apply (Arg a) 

Instances

type Elim = Elim' Term #

type Elims = [Elim] #

data Abs a #

Constructors

Abs String a 

Instances

Show a => Show (Abs a) # 

Methods

showsPrec :: Int -> Abs a -> ShowS #

show :: Abs a -> String #

showList :: [Abs a] -> ShowS #

Unquote a => Unquote (Abs a) # 

Methods

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

ToAbstract r a => ToAbstract (Abs r) (a, Name) # 

Methods

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

type Type = Term #

data Sort #

Constructors

SetS Term 
LitS Integer 
UnknownS 

Instances