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

Safe HaskellNone
LanguageHaskell98

Agda.Syntax.Info

Description

An info object contains additional information about a piece of abstract syntax that isn't part of the actual syntax. For instance, it might contain the source code position of an expression or the concrete syntax that an internal expression originates from.

Synopsis

Documentation

data ModuleInfo Source #

Constructors

ModuleInfo 

Fields

mkDefInfoInstance :: Name -> Fixity' -> Access -> IsAbstract -> IsInstance -> IsMacro -> Range -> DefInfo Source #

Same as mkDefInfo but where we can also give the IsInstance

newtype PatInfo Source #

For a general pattern we remember the source code position.

Constructors

PatRange Range 

patNoRange :: PatInfo Source #

Empty range for patterns.

data ConPatInfo Source #

Constructor pattern info.

Constructors

ConPatInfo 

Fields