Agda-2.6.1.3: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Utils.Haskell.Syntax

Description

ASTs for subset of GHC Haskell syntax.

Synopsis

Modules

data Module Source #

Instances

Instances details
Pretty Module Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

data ModulePragma Source #

Constructors

LanguagePragma [Name] 
OtherPragma String

Unstructured pragma (Andreas, 2017-08-23, issue #2712).

Instances

Instances details
Pretty ModulePragma Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

data ImportSpec Source #

Constructors

IVar Name 

Instances

Instances details
Pretty ImportSpec Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Declarations

data Decl Source #

Instances

Instances details
Eq Decl Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

(==) :: Decl -> Decl -> Bool #

(/=) :: Decl -> Decl -> Bool #

Pretty Decl Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

data DataOrNew Source #

Constructors

DataType 
NewType 

Instances

Instances details
Eq DataOrNew Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Pretty DataOrNew Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

data ConDecl Source #

Constructors

ConDecl Name [(Maybe Strictness, Type)] 

Instances

Instances details
Eq ConDecl Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

(==) :: ConDecl -> ConDecl -> Bool #

(/=) :: ConDecl -> ConDecl -> Bool #

Pretty ConDecl Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

data Strictness Source #

Constructors

Lazy 
Strict 

Instances

Instances details
Eq Strictness Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Pretty Strictness Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

type Deriving = (QName, [Type]) Source #

data Binds Source #

Constructors

BDecls [Decl] 

Instances

Instances details
Eq Binds Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

(==) :: Binds -> Binds -> Bool #

(/=) :: Binds -> Binds -> Bool #

Pretty Binds Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

data Rhs Source #

Instances

Instances details
Eq Rhs Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

(==) :: Rhs -> Rhs -> Bool #

(/=) :: Rhs -> Rhs -> Bool #

data GuardedRhs Source #

Constructors

GuardedRhs [Stmt] Exp 

Instances

Instances details
Eq GuardedRhs Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

data Match Source #

Constructors

Match Name [Pat] Rhs (Maybe Binds) 

Instances

Instances details
Eq Match Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

(==) :: Match -> Match -> Bool #

(/=) :: Match -> Match -> Bool #

Pretty Match Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Expressions

data Type Source #

Instances

Instances details
Eq Type Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

(==) :: Type -> Type -> Bool #

(/=) :: Type -> Type -> Bool #

Pretty Type Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

data Pat Source #

Instances

Instances details
Eq Pat Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

(==) :: Pat -> Pat -> Bool #

(/=) :: Pat -> Pat -> Bool #

Pretty Pat Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

data Stmt Source #

Constructors

Qualifier Exp 
Generator Pat Exp 

Instances

Instances details
Eq Stmt Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

(==) :: Stmt -> Stmt -> Bool #

(/=) :: Stmt -> Stmt -> Bool #

Pretty Stmt Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

data Exp Source #

Instances

Instances details
Eq Exp Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

(==) :: Exp -> Exp -> Bool #

(/=) :: Exp -> Exp -> Bool #

Pretty Exp Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

data Alt Source #

Constructors

Alt Pat Rhs (Maybe Binds) 

Instances

Instances details
Eq Alt Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

(==) :: Alt -> Alt -> Bool #

(/=) :: Alt -> Alt -> Bool #

Pretty Alt Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

data Literal Source #

Instances

Instances details
Eq Literal Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

(==) :: Literal -> Literal -> Bool #

(/=) :: Literal -> Literal -> Bool #

Pretty Literal Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Names

data QName Source #

Constructors

Qual ModuleName Name 
UnQual Name 

Instances

Instances details
Eq QName Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

(==) :: QName -> QName -> Bool #

(/=) :: QName -> QName -> Bool #

Pretty QName Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

data Name Source #

Constructors

Ident String 
Symbol String 

Instances

Instances details
Eq Name Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

(==) :: Name -> Name -> Bool #

(/=) :: Name -> Name -> Bool #

Pretty Name Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

data QOp Source #

Constructors

QVarOp QName 

Instances

Instances details
Eq QOp Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

(==) :: QOp -> QOp -> Bool #

(/=) :: QOp -> QOp -> Bool #

Pretty QOp Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

data TyVarBind Source #

Constructors

UnkindedVar Name 

Instances

Instances details
Eq TyVarBind Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Pretty TyVarBind Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty