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

Safe HaskellSafe
LanguageHaskell2010

Agda.Utils.Haskell.Syntax

Documentation

data ImportSpec Source #

Constructors

IVar Name 

data DataOrNew Source #

Constructors

DataType 
NewType 

Instances

data ConDecl Source #

Constructors

ConDecl Name [Type] 

Instances

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

data Binds Source #

Constructors

BDecls [Decl] 

Instances

Eq Binds Source # 

Methods

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

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

data Rhs Source #

Instances

Eq Rhs Source # 

Methods

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

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

data Match Source #

Constructors

Match Name [Pat] Rhs (Maybe Binds) 

Instances

Eq Match Source # 

Methods

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

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

data Stmt Source #

Constructors

Qualifier Exp 
Generator Pat Exp 

Instances

Eq Stmt Source # 

Methods

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

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

data Alt Source #

Constructors

Alt Pat Rhs (Maybe Binds) 

Instances

Eq Alt Source # 

Methods

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

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

data Literal Source #

Instances

data QName Source #

Constructors

Qual ModuleName Name 
UnQual Name 

Instances

Eq QName Source # 

Methods

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

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

data Name Source #

Constructors

Ident String 
Symbol String 

Instances

Eq Name Source # 

Methods

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

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

data QOp Source #

Constructors

QVarOp QName 

Instances

Eq QOp Source # 

Methods

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

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

data TyVarBind Source #

Constructors

UnkindedVar Name 

Instances