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

Safe HaskellNone

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 posisiton of an expression or the concrete syntax that an internal expression originates from.

Synopsis

Documentation

data Info Source

Constructors

Nope 

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