Agda.Syntax.Concrete

ex: x

ex: 1 or "foo"

ex: ? or {! ... !}

ex: _ or _A_5

before parsing operators

ex: e e, e {e}, or e {x = e}

ex: e + e The QName is possibly ambiguous, but it must correspond to one of the names in the set.

ex: e | e1 | .. | en

ex: {e} or {x=e}

ex: {{e}} or {{x=e}}

ex: \x {y} -> e or \(x:A){y:B} -> e

ex: \ ()

ex: \ { p11 .. p1a -> e1 ; .. ; pn1 .. pnz -> en }

ex: e -> e or .e -> e (NYI: {e} -> e)

ex: (xs:e) -> e or {xs:e} -> e

ex: record {x = a; y = b}, or record { x = a; M1; M2 } The KwRange is for the record keyword.

ex: record e {x = a; y = b} The KwRange is for the record keyword.

ex: let Ds in e, missing body when parsing do-notation let

ex: (e)

ex: (| e1 | e2 | .. | en |) or (|)

ex: do x <- m1; m2

ex: () or {}, only in patterns

ex: x@p, only in patterns

ex: .p, only in patterns

ex: ..A, used for parsing ..A -> B

ex: quote, should be applied to a name

ex: quoteTerm, should be applied to a term

ex: @(tactic t), used to declare tactic arguments

ex: unquote, should be applied to a term of type Term

to print irrelevant things

ex: a = b, used internally in the parser

..., used internally to parse patterns.

An identifier coming from abstract syntax, for which we know a precise syntactic highlighting class (used in printing).

An operator application coming from abstract syntax, for which we know a precise syntactic highlighting class (used in printing).

An abstraction inside a special syntax declaration (see Issue 358 why we introduce this).

. x or {x} or .x or .{x} or {.x} or x@p or (p)

. (xs : e) or {xs : e}

Binding (x1@p1 ... xn@pn : A).

Let binding (let Ds) or (open M args).

Axioms and functions can be irrelevant. (Hiding should be NotHidden)

Variables to be generalized, can be hidden and/or irrelevant.

lone data signature in mutual block

lone record signature in mutual block

notation declaration for a name

In Agda.Syntax.Concrete.Definitions we generate private blocks temporarily, which should be treated different that user-declared private blocks. Thus the Origin.

The KwRange here only refers to the range of the instance keyword. The range of the whole block InstanceB r ds is fuseRange r ds.

Range of keyword [co]inductive.

Range of [no-]eta-equality keyword.

If declaration pattern is present, give its range.

tel M exprs where M exprs is a RawApp just after parsing.

Original pattern (including with-patterns), rewrite equations and with-expressions.

c or x

If the boolean is False, then the QName must not refer to a constructor or a pattern synonym. The value False is used when a hidden argument pun is expanded.

p p' or p {x = p'}

p1..pn before parsing operators

eg: p => p' for operator _=>_ The QName is possibly ambiguous, but it must correspond to one of the names in the set.

{p} or {x = p}

{{p}} or {{x = p}}

.e, the KwRange is for the dot, the Range for the whole thing (including the dot).

0, 1, etc.

record {x = p; y = q}. The KwRange is for the record keyword.

i = i1 i.e. cubical face lattice generator

..., only as left-most pattern. Second arg is Nothing before expansion, and Just p after expanding ellipsis to p.

| p, for with-patterns.

No right hand side because of absurd match.

No where clauses.

Ordinary where. Range of the where keyword. List of declarations can be empty.

Named where: module M where ds. Range of the keywords module and where. The Access flag applies to the Name (not the module contents!) and is propagated from the parent function. List of declarations can be empty.

No where clauses.

Ordinary where.

Named where: module M where ....

Second Range is for REWRITE keyword.

INLINE or NOINLINE

Throws an internal error in the scope checker. The Strings are words to be displayed with the error.

For coinductive records, use pragma instead of regular eta-equality definition (as it is might make Agda loop).

Applies to the named function

Applies to the current module

Mark a definition as injective for the pattern matching unifier.

Mark a definition as injective for the conversion checker

Display lhs as rhs (modifies the printer).

Applies to the following function clause.

Applies to the following function (and all that are mutually recursive with it) or to the functions in the following mutual block.

Applies to the following function (and all that are mutually recursive with it) or to the functions in the following mutual block.

Applies to the following data/record type or mutual block.

Applies to the following data/record type.

Applies to the stated function

Applies to the given name(s), which must be instance names (checked by the type checker).