Agda-2.4.0.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 ExprInfo Source

For a general expression we can either remember just the source code position or the entire concrete expression it came from.

Constructors

ExprRange Range 
ExprSource Range (Precedence -> Expr)

Even if we store the original expression we have to know whether to put parenthesis around it.

data MutualInfo Source

Constructors

MutualInfo 

Fields

mutualTermCheck :: Bool

termination check (default=True)

mutualRange :: Range
 

patNoRange :: PatInfo Source

Empty range for patterns.

data ConPatInfo Source

Constructor pattern info.

Constructors

ConPatInfo 

Fields

patImplicit :: Bool

Does this pattern come form the eta-expansion of an implicit pattern.

patInfo :: PatInfo