- data NiceDeclaration
- = Axiom Range Fixity Access IsAbstract Name Expr
- | NiceField Range Fixity Access IsAbstract Hiding Name Expr
- | PrimitiveFunction Range Fixity Access IsAbstract Name Expr
- | NiceDef Range [Declaration] [NiceTypeSignature] [NiceDefinition]
- | NiceModule Range Access IsAbstract QName Telescope [Declaration]
- | NiceModuleMacro Range Access IsAbstract Name Telescope Expr OpenShortHand ImportDirective
- | NiceOpen Range QName ImportDirective
- | NiceImport Range QName (Maybe AsName) OpenShortHand ImportDirective
- | NicePragma Range Pragma
- data NiceDefinition
- type NiceConstructor = NiceTypeSignature
- type NiceTypeSignature = NiceDeclaration
- data Clause = Clause Name LHS RHS WhereClause [Clause]
- data DeclarationException
- type Nice = Either DeclarationException
- runNice :: Nice a -> Either DeclarationException a
- niceDeclarations :: [Declaration] -> Nice [NiceDeclaration]
- notSoNiceDeclarations :: [NiceDeclaration] -> [Declaration]
Documentation
data NiceDeclaration Source
The nice declarations. No fixity declarations and function definitions are
contained in a single constructor instead of spread out between type
signatures and clauses. The private
, postulate
, and abstract
modifiers have been distributed to the individual declarations.
Axiom Range Fixity Access IsAbstract Name Expr | |
NiceField Range Fixity Access IsAbstract Hiding Name Expr | |
PrimitiveFunction Range Fixity Access IsAbstract Name Expr | |
NiceDef Range [Declaration] [NiceTypeSignature] [NiceDefinition] | A bunch of mutually recursive functions/datatypes. The last two lists have the same length. The first list is the concrete declarations these definitions came from. |
NiceModule Range Access IsAbstract QName Telescope [Declaration] | |
NiceModuleMacro Range Access IsAbstract Name Telescope Expr OpenShortHand ImportDirective | |
NiceOpen Range QName ImportDirective | |
NiceImport Range QName (Maybe AsName) OpenShortHand ImportDirective | |
NicePragma Range Pragma |
data NiceDefinition Source
A definition without its type signature.
FunDef Range [Declaration] Fixity Access IsAbstract Name [Clause] | |
DataDef Range Induction Fixity Access IsAbstract Name [LamBinding] [NiceConstructor] | |
RecDef Range Fixity Access IsAbstract Name (Maybe NiceConstructor) [LamBinding] [NiceDeclaration] | The |
type NiceConstructor = NiceTypeSignatureSource
Only Axiom
s.
type NiceTypeSignature = NiceDeclarationSource
Only Axiom
s.
data DeclarationException Source
The exception type.
type Nice = Either DeclarationExceptionSource
runNice :: Nice a -> Either DeclarationException aSource
niceDeclarations :: [Declaration] -> Nice [NiceDeclaration]Source