|
|
|
Description |
The abstract syntax. This is what you get after desugaring and scope
analysis of the concrete syntax. The type checker works on abstract syntax,
producing internal syntax (Agda.Syntax.Internal).
|
|
Synopsis |
|
|
|
Documentation |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
A definition without its type signature.
| Constructors | |
|
|
|
Only Axioms.
|
|
|
|
|
A lambda binding is either domain free or typed.
| Constructors | |
|
|
|
Typed bindings with hiding information.
| Constructors | |
|
|
|
A typed binding. Appears in dependent function spaces, typed lambdas, and
telescopes. I might be tempting to simplify this to only bind a single
name at a time. This would mean that we would have to typecheck the type
several times (x,y:A vs. x:A; y:A). In most cases this wouldn't
really be a problem, but it's good principle to not do extra work unless
you have to.
| Constructors | |
|
|
|
|
|
We could throw away where clauses at this point and translate them to
let. It's not obvious how to remember that the let was really a
where clause though, so for the time being we keep it here.
| Constructors | |
|
|
|
|
|
|
|
|
|
Parameterised over the type of dot patterns.
| Constructors | |
|
|
|
|
|
Extracts all the names which are declared in a Declaration.
This does not include open public or let expressions, but it does
include local modules and where clauses.
|
|
|
The name defined by the given axiom.
Precondition: The declaration has to be an Axiom.
|
|
module Agda.Syntax.Abstract.Name |
|
Produced by Haddock version 2.6.1 |