Agda-2.6.1: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Compiler.JS.Syntax

Documentation

data Exp Source #

Instances

Instances details
Show Exp Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Globals Exp Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Uses Exp Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

uses :: Exp -> Set [MemberId] Source #

Pretty Exp Source # 
Instance details

Defined in Agda.Compiler.JS.Pretty

Methods

pretty :: Nat -> Int -> Exp -> String Source #

newtype LocalId Source #

Constructors

LocalId Nat 

Instances

Instances details
Eq LocalId Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Ord LocalId Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Show LocalId Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Pretty LocalId Source # 
Instance details

Defined in Agda.Compiler.JS.Pretty

Methods

pretty :: Nat -> Int -> LocalId -> String Source #

data Export Source #

Constructors

Export 

Fields

Instances

Instances details
Show Export Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Globals Export Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Uses Export Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

uses :: Export -> Set [MemberId] Source #

data Module Source #

Constructors

Module 

Instances

Instances details
Show Module Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Globals Module Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Pretty Module Source # 
Instance details

Defined in Agda.Compiler.JS.Pretty

Methods

pretty :: Nat -> Int -> Module -> String Source #

class Uses a where Source #

Methods

uses :: a -> Set [MemberId] Source #

Instances

Instances details
Uses Export Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

uses :: Export -> Set [MemberId] Source #

Uses Exp Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

uses :: Exp -> Set [MemberId] Source #

Uses a => Uses [a] Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

uses :: [a] -> Set [MemberId] Source #

Uses a => Uses (Map k a) Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

uses :: Map k a -> Set [MemberId] Source #

class Globals a where Source #

Methods

globals :: a -> Set GlobalId Source #

Instances

Instances details
Globals Module Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Globals Export Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Globals Exp Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Globals a => Globals [a] Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

globals :: [a] -> Set GlobalId Source #

Globals a => Globals (Map k a) Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

globals :: Map k a -> Set GlobalId Source #