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

- data Induction
  - = Inductive
  - | CoInductive
- data Hiding
  - = Hidden
  - | NotHidden
- data Relevance
  - = Relevant
  - | Irrelevant
  - | Forced
- ignoreForced :: Relevance -> Relevance
- irrelevant :: Bool -> Relevance
- data Arg e = Arg {
  - argHiding :: Hiding
  - argRelevance :: Relevance
  - unArg :: e
  }
- hide :: Arg a -> Arg a
- defaultArg :: a -> Arg a
- isHiddenArg :: Arg a -> Bool
- makeIrrelevant :: Arg a -> Arg a
- makeRelevant :: Arg a -> Arg a
- withArgsFrom :: [a] -> [Arg b] -> [Arg a]
- 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

Constructors

Inductive |
CoInductive |

Instances

Eq Induction |
Data Induction |
Ord Induction |
Show Induction |
Typeable Induction |
Arbitrary Induction |
CoArbitrary Induction |
Pretty Induction |
KillRange Induction |
EmbPrj Induction |

data Hiding

Constructors

Hidden |
NotHidden |

Instances

Eq Hiding |
Data Hiding |
Ord Hiding |
Show Hiding |
Typeable Hiding |
KillRange Hiding |
GenC Hiding |
EmbPrj Hiding |
ShrinkC Hiding Hiding |

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

Instances

Eq Relevance |
Data Relevance |
Ord Relevance |
Show Relevance |
Typeable Relevance |
Pretty Relevance |
KillRange Relevance |
EmbPrj Relevance |
PrettyTCM Relevance |

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 |

Fields

argHiding :: Hiding
argRelevance :: Relevance
unArg :: e

Instances

Functor Arg |
Typeable1 Arg |
Foldable Arg |
Traversable Arg |
Abstract Telescope |
KillVar Telescope |
GenC Telescope |
EmbPrj Telescope |
Reduce Telescope |
Instantiate Telescope |
PrettyTCM Telescope |
ShrinkC Telescope Telescope |
Reify Telescope Telescope |
Eq a => Eq (Arg a) |
Data e => Data (Arg e) |
Ord e => Ord (Arg e) |
Show a => Show (Arg a) |
Sized a => Sized (Arg a) |
Pretty e => Pretty (Arg e) |
KillRange a => KillRange (Arg a) |
HasRange a => HasRange (Arg a) |
Free a => Free (Arg a) |
TermLike a => TermLike (Arg a) |
Strict a => Strict (Arg a) |
Raise t => Raise (Arg t) |
Subst a => Subst (Arg a) |
AbstractTerm a => AbstractTerm (Arg a) |
KillVar a => KillVar (Arg a) |
GenC a => GenC (Arg a) |
EmbPrj a => EmbPrj (Arg a) |
InstantiateFull t => InstantiateFull (Arg t) |
Normalise t => Normalise (Arg t) |
Reduce t => Reduce (Arg t) |
Instantiate t => Instantiate (Arg t) |
Match a => Match (Arg a) |
DotVars a => DotVars (Arg a) |
(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Arg a) |
Occurs a => Occurs (Arg a) |
ComputeOccurrences a => ComputeOccurrences (Arg a) |
HasPolarity a => HasPolarity (Arg a) |
LowerMeta a => LowerMeta (Arg a) |
ToConcrete a c => ToConcrete (Arg a) (Arg c) |
ToAbstract c a => ToAbstract (Arg c) (Arg a) |
ShrinkC a b => ShrinkC (Arg a) (Arg b) |
Reify i a => Reify (Arg i) (Arg a) |

hide :: Arg a -> Arg a

defaultArg :: a -> Arg a

isHiddenArg :: Arg a -> Bool

makeIrrelevant :: Arg a -> Arg a

makeRelevant :: Arg a -> Arg a

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

`xs `withArgsFrom` args` translates `xs` into a list of `Arg`s, 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 |

Instances

Eq IsInfix |
Data IsInfix |
Ord IsInfix |
Show IsInfix |
Typeable IsInfix |

data Access

Access modifier.

Constructors

PrivateAccess |
PublicAccess |

Instances

Eq Access |
Data Access |
Ord Access |
Show Access |
Typeable Access |
EmbPrj Access |

data IsAbstract

Abstract or concrete

Constructors

AbstractDef |
ConcreteDef |

Instances

Eq IsAbstract |
Data IsAbstract |
Ord IsAbstract |
Show IsAbstract |
Typeable IsAbstract |
EmbPrj IsAbstract |

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 |

Instances

Enum NameId |
Eq NameId |
Data NameId |
Ord NameId |
Show NameId |
Typeable NameId |
EmbPrj NameId |
HasFresh NameId FreshThings |

newtype Constr a

Constructors

Constr a |

Instances

ToConcrete (Constr Constructor) Declaration |