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

Safe HaskellSafe
LanguageHaskell2010

Agda.Utils.Haskell.Syntax

Documentation

data ModulePragma #

Constructors

LanguagePragma [Name] 

data ImportSpec #

Constructors

IVar Name 

data DataOrNew #

Constructors

DataType 
NewType 

Instances

data ConDecl #

Constructors

ConDecl Name [Type] 

Instances

Eq ConDecl # 

Methods

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

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

type Deriving = (QName, [Type]) #

data Binds #

Constructors

BDecls [Decl] 

Instances

Eq Binds # 

Methods

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

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

data Rhs #

Instances

Eq Rhs # 

Methods

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

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

data GuardedRhs #

Constructors

GuardedRhs [Stmt] Exp 

data Match #

Constructors

Match Name [Pat] Rhs (Maybe Binds) 

Instances

Eq Match # 

Methods

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

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

data Type #

Instances

Eq Type # 

Methods

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

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

data Pat #

Instances

Eq Pat # 

Methods

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

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

data Stmt #

Constructors

Qualifier Exp 
Generator Pat Exp 

Instances

Eq Stmt # 

Methods

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

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

data Alt #

Constructors

Alt Pat Rhs (Maybe Binds) 

Instances

Eq Alt # 

Methods

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

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

data Literal #

Instances

Eq Literal # 

Methods

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

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

data QName #

Constructors

Qual ModuleName Name 
UnQual Name 

Instances

Eq QName # 

Methods

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

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

data Name #

Constructors

Ident String 
Symbol String 

Instances

Eq Name # 

Methods

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

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

data QOp #

Constructors

QVarOp QName 

Instances

Eq QOp # 

Methods

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

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

data TyVarBind #

Constructors

UnkindedVar Name 

Instances