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

Agda.Syntax.Common

Description

Some common syntactic entities are defined in this module.

Synopsis

Documentation

data Relevance

A function argument can be relevant or irrelevant.

Constructors

Relevant

the argument is (possibly) relevant at compile-time

Irrelevant

the argument is irrelevant at compile- and runtime

Forced

the argument can be skipped during equality checking

ignoreForced :: Relevance -> Relevance

For comparing Relevance ignoring Forced.

irrelevant :: Bool -> Relevance

Relevance from Bool.

data Arg e

A function argument can be hidden and/or irrelevant.

Constructors

Arg 

hide :: Arg a -> Arg a

defaultArg :: a -> Arg a

makeRelevant :: Arg a -> Arg a

withArgsFrom :: [a] -> [Arg b] -> [Arg a]

xs withArgsFrom args translates xs into a list of Args, using the elements in args to fill in the non-unArg fields.

Precondition: The two lists should have equal length.

data Named name a

Constructors

Named 

Fields

nameOf :: Maybe name
 
namedThing :: a
 

Instances

Typeable2 Named 
Functor (Named name) 
Foldable (Named name) 
Traversable (Named name) 
(Eq name, Eq a) => Eq (Named name a) 
(Data name, Data a) => Data (Named name a) 
(Ord name, Ord a) => Ord (Named name a) 
Show a => Show (Named String a) 
Sized a => Sized (Named name a) 
Pretty e => Pretty (Named String e) 
KillRange a => KillRange (Named name a) 
HasRange a => HasRange (Named name a) 
DotVars a => DotVars (Named s a) 
LowerMeta a => LowerMeta (Named name a) 
ToConcrete a c => ToConcrete (Named name a) (Named name c) 
ToAbstract c a => ToAbstract (Named name c) (Named name a) 

unnamed :: a -> Named name a

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

type NamedArg a = Arg (Named String a)

Only Hidden arguments can have names.

data IsInfix

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

Constructors

InfixDef 
PrefixDef 

data Access

Access modifier.

type Nat = Integer

type Arity = Nat

data NameId

The unique identifier of a name. Second argument is the top-level module identifier.

Constructors

NameId Nat Integer 

newtype Constr a

Constructors

Constr a