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

Safe Haskell | None
Language | Haskell2010

Agda.Syntax.Reflected

# Documentation

type Args = [Arg Term] Source #

data Elim' a Source #

Constructors

Apply (Arg a) |

#### Instances

Instances details

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

Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Expr, Elim) |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef (Expr, Elim) = Expr

Methods

toAbstract :: MonadReflectedToAbstract m => (Expr, Elim) -> m (AbsOfRef (Expr, Elim)) Source #

ToAbstract (Expr, Elims) Source # |

Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Expr, Elims) |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef (Expr, Elims) = Expr

Methods

toAbstract :: MonadReflectedToAbstract m => (Expr, Elims) -> m (AbsOfRef (Expr, Elims)) Source #

type AbsOfRef (Expr, Elim) Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef (Expr, Elim) = Expr
type AbsOfRef (Expr, Elims) Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef (Expr, Elims) = Expr

type Elim = Elim' Term Source #

type Elims = [Elim] Source #

argsToElims :: Args -> Elims Source #

data Abs a Source #

Constructors

Abs String a |

#### Instances

Instances details

ToAbstract r => ToAbstract (Abs r) Source # |

Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Abs r) |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef (Abs r) = (AbsOfRef r, Name)

Methods

toAbstract :: MonadReflectedToAbstract m => Abs r -> m (AbsOfRef (Abs r)) Source #

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

data Term Source #

Constructors

Var Int Elims |
Con QName Elims |
Def QName Elims |
Meta MetaId Elims |
Lam Hiding (Abs Term) |
ExtLam (List1 Clause) Elims |
Pi (Dom Type) (Abs Type) |
Sort Sort |
Lit Literal |
Unknown |

#### Instances

Instances details

ToAbstract Term Source # |

Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef Term |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef Term = Expr

Methods

toAbstract :: MonadReflectedToAbstract m => Term -> m (AbsOfRef Term) Source #

Unquote Elim Source # |
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM Elim Source #
Unquote Term Source # |
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM Term Source #
Show Term Source # |
Instance details Defined in Agda.Syntax.Reflected Methods showsPrec :: Int -> Term -> ShowS Source # show :: Term -> String Source # showList :: [Term] -> ShowS Source #
ToAbstract (Expr, Elim) Source # |

Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Expr, Elim) |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef (Expr, Elim) = Expr

Methods

toAbstract :: MonadReflectedToAbstract m => (Expr, Elim) -> m (AbsOfRef (Expr, Elim)) Source #

ToAbstract (Expr, Elims) Source # |

Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Expr, Elims) |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef (Expr, Elims) = Expr

Methods

toAbstract :: MonadReflectedToAbstract m => (Expr, Elims) -> m (AbsOfRef (Expr, Elims)) Source #

type AbsOfRef Term Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef Term = Expr
type AbsOfRef (Expr, Elim) Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef (Expr, Elim) = Expr
type AbsOfRef (Expr, Elims) Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef (Expr, Elims) = Expr

type Type = Term Source #

data Sort Source #

Constructors

SetS Term |
LitS Integer |
PropS Term |
PropLitS Integer |
InfS Integer |
UnknownS |

#### Instances

Instances details

ToAbstract Sort Source # |

Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef Sort |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef Sort = Expr

Methods

toAbstract :: MonadReflectedToAbstract m => Sort -> m (AbsOfRef Sort) Source #

Unquote Sort Source # |
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM Sort Source #
Show Sort Source # |
Instance details Defined in Agda.Syntax.Reflected Methods showsPrec :: Int -> Sort -> ShowS Source # show :: Sort -> String Source # showList :: [Sort] -> ShowS Source #
type AbsOfRef Sort Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef Sort = Expr

data Pattern Source #

Constructors

ConP QName [Arg Pattern] |
DotP Term |
VarP Int |
LitP Literal |
AbsurdP Int |
ProjP QName |

#### Instances

Instances details

ToAbstract Pattern Source # |

Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef Pattern |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef Pattern = Pattern

Methods

toAbstract :: MonadReflectedToAbstract m => Pattern -> m (AbsOfRef Pattern) Source #

Unquote Pattern Source # |
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM Pattern Source #
Show Pattern Source # |
Instance details Defined in Agda.Syntax.Reflected Methods showsPrec :: Int -> Pattern -> ShowS Source # show :: Pattern -> String Source # showList :: [Pattern] -> ShowS Source #
type AbsOfRef Pattern Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef Pattern = Pattern

data Clause Source #

Constructors

Clause |

Fields

- clauseTel :: [(Text, Arg Type)]
- clausePats :: [Arg Pattern]
- clauseRHS :: Term

AbsurdClause |

Fields

- clauseTel :: [(Text, Arg Type)]
- clausePats :: [Arg Pattern]

#### Instances

Instances details

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

Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (QNamed Clause) |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef (QNamed Clause) = Clause

Methods

toAbstract :: MonadReflectedToAbstract m => QNamed Clause -> m (AbsOfRef (QNamed Clause)) Source #

ToAbstract (List1 (QNamed Clause)) Source # |

Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (List1 (QNamed Clause)) |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef (List1 (QNamed Clause)) = List1 Clause

Methods

toAbstract :: MonadReflectedToAbstract m => List1 (QNamed Clause) -> m (AbsOfRef (List1 (QNamed Clause))) Source #

ToAbstract [QNamed Clause] Source # |

Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef [QNamed Clause] |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef [QNamed Clause] = [Clause]

Methods

toAbstract :: MonadReflectedToAbstract m => [QNamed Clause] -> m (AbsOfRef [QNamed Clause]) Source #

type AbsOfRef (QNamed Clause) Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef (QNamed Clause) = Clause
type AbsOfRef (List1 (QNamed Clause)) Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef (List1 (QNamed Clause)) = List1 Clause
type AbsOfRef [QNamed Clause] Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef [QNamed Clause] = [Clause]

data Definition Source #

Constructors

FunDef Type [Clause] |
DataDef |
RecordDef |
DataConstructor |
Axiom |
Primitive |

#### Instances

Instances details

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