Agda-2.2.6: A dependently typed functional programming language and proof assistant Source code Contents Index

Agda.Syntax.Common

Description

Some common syntactic entities are defined in this module.

Synopsis

data Induction = Inductive | CoInductive data Hiding = Hidden | NotHidden data Arg e = Arg { argHiding :: Hiding unArg :: e } data Named name a = Named { nameOf :: Maybe name namedThing :: a } unnamed :: a -> Named name a named :: name -> a -> Named name a type NamedArg a = Arg (Named String a) data IsInfix = InfixDef | PrefixDef data Access = PrivateAccess | PublicAccess data IsAbstract = AbstractDef | ConcreteDef type Nat = Integer type Arity = Nat data NameId = NameId Nat Integer newtype Constr a = Constr a

Documentation

data Induction Source

Constructors Inductive CoInductive

data Hiding Source

Constructors Hidden NotHidden

data Arg e Source

A function argument can be hidden. Constructors Arg argHiding :: Hiding unArg :: e

data Named name a Source

Constructors Named nameOf :: Maybe name namedThing :: a

unnamed :: a -> Named name a Source

named :: name -> a -> Named name a Source

type NamedArg a = Arg (Named String a) Source

Only Hidden arguments can have names.

data IsInfix Source

Functions can be defined in both infix and prefix style. See Agda.Syntax.Concrete.LHS. Constructors InfixDef PrefixDef

data Access Source

Access modifier. Constructors PrivateAccess PublicAccess

data IsAbstract Source

Abstract or concrete Constructors AbstractDef ConcreteDef

type Nat = Integer Source

type Arity = Nat Source

data NameId Source

The unique identifier of a name. Second argument is the top-level module identifier. Constructors NameId Nat Integer

newtype Constr a Source

Constructors Constr a

Produced by Haddock version 2.6.0