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

Safe HaskellNone

Agda.Syntax.Translation.ConcreteToAbstract

Description

Translation from Agda.Syntax.Concrete to Agda.Syntax.Abstract. Involves scope analysis, figuring out infix operator precedences and tidying up definitions.

Synopsis

Documentation

localToAbstract :: ToAbstract c a => c -> (a -> ScopeM b) -> ScopeM b

This operation does not affect the scope, i.e. the original scope is restored upon completion.

newtype OldName

Constructors

OldName Name 

newtype TopLevel a

Constructors

TopLevel a 

topLevelModuleName :: TopLevelInfo -> ModuleName

The top-level module name.