ModuleAgda-2.7.0.1Haskell2010

Agda.TypeChecking.SizedTypes.Syntax

Syntax of size expressions and constraints.

18 types
5 classes
7 values

PackageAgda-2.7.0.1
Exports30
LanguageHaskell2010
LicenceMIT
SourceSyntax.hs

Syntax

8 declarations

newtypenewtype Offset

Constant finite sizes n >= 0.

Constructors

O Int

Instances17Enum, Eq, Num, Ord, Show, Generic, …

Enum OffsetDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Eq OffsetDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Num OffsetDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Ord OffsetDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Show OffsetDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Generic OffsetDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
NFData OffsetDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Pretty OffsetDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
TruncateOffset OffsetDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
ValidOffset OffsetDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
MeetSemiLattice OffsetDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Negative OffsetDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver
Plus Offset Offset OffsetDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Plus Offset Weight WeightDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver
Plus Weight Offset WeightDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver
Plus (SizeExpr' r f) Offset (SizeExpr' r f)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Add offset to size expression.
type Rep Offset = D1 ('MetaData "Offset" "Agda.TypeChecking.SizedTypes.Syntax" "Agda-2.7.0.1-DbbZpETDDF1KkwuzEZvfn8" 'True) (C1 ('MetaCons "O" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)))Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax

newtypenewtype Rigid

Fixed size variables i.

Constructors

RigidId
- rigidId :: String

Instances4Eq, Ord, Show, Pretty

Eq RigidDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Ord RigidDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Show RigidDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Pretty RigidDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax

newtypenewtype Flex

Size meta variables X to solve for.

Constructors

FlexId
- flexId :: String

Instances4Eq, Ord, Show, Pretty

Eq FlexDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Ord FlexDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Show FlexDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Pretty FlexDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax

datadata SizeExpr' rigid flex

Size expressions appearing in constraints.

Constructors

Const
Constant number n.
- offset :: Offset
Rigid
Variable plus offset i + n.
- rigid :: rigid
- offset :: Offset
Infty
Infinity ∞.
Flex
Meta variable X + n.
- flex :: flex
- offset :: Offset

Instances22Substitute, Functor, Foldable, Traversable, Eq, Ord, …

Ord f => Substitute r f (SizeExpr' r f)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Functor (SizeExpr' rigid)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Foldable (SizeExpr' rigid)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Traversable (SizeExpr' rigid)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
(Eq rigid, Eq flex) => Eq (SizeExpr' rigid flex)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
(Ord rigid, Ord flex) => Ord (SizeExpr' rigid flex)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
(Show rigid, Show flex) => Show (SizeExpr' rigid flex)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Generic (SizeExpr' rigid flex)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
(NFData r, NFData f) => NFData (SizeExpr' r f)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
(Pretty r, Pretty f) => Pretty (SizeExpr' r f)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Subst (SizeExpr' NamedRigid SizeMeta)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Solve · orphan
Only for raise.
Ord flex => Flexs (SizeExpr' rigid flex)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Ord r => Rigids (SizeExpr' r f)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
TruncateOffset (SizeExpr' r f)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
ValidOffset (SizeExpr' r f)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Plus (SizeExpr' r f) Offset (SizeExpr' r f)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Add offset to size expression.
Plus (SizeExpr' r f) Label (SizeExpr' r f)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver
Plus (SizeExpr' r f) Weight (SizeExpr' r f)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver
type Rep (SizeExpr' rigid flex) = D1 ('MetaData "SizeExpr'" "Agda.TypeChecking.SizedTypes.Syntax" "Agda-2.7.0.1-DbbZpETDDF1KkwuzEZvfn8" 'False) ((C1 ('MetaCons "Const" 'PrefixI 'True) (S1 ('MetaSel ('Just "offset") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Offset)) :+: C1 ('MetaCons "Rigid" 'PrefixI 'True) (S1 ('MetaSel ('Just "rigid") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 rigid) :*: S1 ('MetaSel ('Just "offset") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Offset))) :+: (C1 ('MetaCons "Infty" 'PrefixI 'False) U1 :+: C1 ('MetaCons "Flex" 'PrefixI 'True) (S1 ('MetaSel ('Just "flex") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 flex) :*: S1 ('MetaSel ('Just "offset") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Offset))))Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
type SubstArg (SizeExpr' NamedRigid SizeMeta) = TermDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Solve · orphan
type FlexOf (SizeExpr' rigid flex) = flexDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
type RigidOf (SizeExpr' r f) = rDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax

typetype SizeExpr = SizeExpr' Rigid Flex

datadata Cmp

Comparison operator, e.g. for size expression.

Constructors

Lt
<.
Le
≤.

Instances12Bounded, Enum, Eq, Ord, Show, Generic, …

Bounded CmpDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Enum CmpDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Eq CmpDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Ord CmpDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Comparison operator is ordered Lt < Le.
Show CmpDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Generic CmpDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
NFData CmpDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Pretty CmpDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Dioid CmpDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
MeetSemiLattice CmpDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Top CmpDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
type Rep Cmp = D1 ('MetaData "Cmp" "Agda.TypeChecking.SizedTypes.Syntax" "Agda-2.7.0.1-DbbZpETDDF1KkwuzEZvfn8" 'False) (C1 ('MetaCons "Lt" 'PrefixI 'False) U1 :+: C1 ('MetaCons "Le" 'PrefixI 'False) U1)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax

datadata Constraint' rigid flex

Constraint: an inequation between size expressions, e.g. X < ∞ or i + 3 ≤ j.

Constructors

Constraint
- leftExpr :: SizeExpr' rigid flex
- cmp :: Cmp
- rightExpr :: SizeExpr' rigid flex

Instances16Subst, PrettyTCM, Substitute, Functor, Foldable, Traversable, …

Subst SizeConstraintDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Solve · orphan
PrettyTCM SizeConstraintDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Pretty · orphan
Assumes we are in the right context.
Ord f => Substitute r f (Constraint' r f)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Functor (Constraint' rigid)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Foldable (Constraint' rigid)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Traversable (Constraint' rigid)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
(Show rigid, Show flex) => Show (Constraint' rigid flex)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Generic (Constraint' rigid flex)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
(NFData r, NFData f) => NFData (Constraint' r f)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
(Pretty r, Pretty f) => Pretty (Constraint' r f)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Ord flex => Flexs (Constraint' rigid flex)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Ord r => Rigids (Constraint' r f)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
type Rep (Constraint' rigid flex) = D1 ('MetaData "Constraint'" "Agda.TypeChecking.SizedTypes.Syntax" "Agda-2.7.0.1-DbbZpETDDF1KkwuzEZvfn8" 'False) (C1 ('MetaCons "Constraint" 'PrefixI 'True) (S1 ('MetaSel ('Just "leftExpr") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (SizeExpr' rigid flex)) :*: (S1 ('MetaSel ('Just "cmp") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Cmp) :*: S1 ('MetaSel ('Just "rightExpr") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (SizeExpr' rigid flex)))))Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
type SubstArg SizeConstraint = TermDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Solve · orphan
type FlexOf (Constraint' rigid flex) = flexDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
type RigidOf (Constraint' r f) = rDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax

typetype Constraint = Constraint' Rigid Flex

Polarities to specify solutions.

6 declarations

datadata Polarity

What type of solution are we looking for?

Least Greatest

Instances3Eq, Ord, Pretty

Eq PolarityDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Ord PolarityDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Pretty PolarityDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax

datadata PolarityAssignment flex

Assigning a polarity to a flexible variable.

Constructors

PolarityAssignment Polarity flex

Instances1Pretty

Pretty flex => Pretty (PolarityAssignment flex)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax

typetype Polarities flex = Map flex Polarity

Type of solution wanted for each flexible.

valueemptyPolarities :: Polarities flex

valuepolaritiesFromAssignments

:: Ord flex
=> [PolarityAssignment flex]
-> Polarities flex

valuegetPolarity :: Ord flex => Polarities flex -> flex -> Polarity

Default polarity is Least.

Solutions.

3 declarations

newtypenewtype Solution rigid flex

Partial substitution from flexible variables to size expression.

Constructors

Solution
- theSolution :: Map flex (SizeExpr' rigid flex)

Instances4Substitute, Show, Pretty, Null

Ord f => Substitute r f (Solution r f)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
(Show flex, Show rigid) => Show (Solution rigid flex)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
(Pretty r, Pretty f) => Pretty (Solution r f)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Null (Solution rigid flex)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax

valueemptySolution :: Solution r f

classclass Substitute r f a where

Executing a substitution.

Methods

subst :: Solution r f -> a -> a

Instances5Substitute

Substitute r f a => Substitute r f [a]Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Substitute r f a => Substitute r f (Map k a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Ord f => Substitute r f (Constraint' r f)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Ord f => Substitute r f (SizeExpr' r f)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Ord f => Substitute r f (Solution r f)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax

Constraint simplification

4 declarations

typetype CTrans r f = Constraint' r f -> Maybe [Constraint' r f]

valuesimplify1 :: (Pretty f, Pretty r, Eq r) => CTrans r f -> CTrans r f

Returns Nothing if the constraint is contradictory.

valueifLe :: Cmp -> a -> a -> a

Le acts as True, Lt as False.

valuecompareOffset :: Offset -> Cmp -> Offset -> Bool

Interpret Cmp as relation on Offset.

Printing

0 declarations

Wellformedness

2 declarations

classclass ValidOffset a where

Offsets + n must be non-negative

Methods

validOffset :: a -> Bool

Instances2ValidOffset

ValidOffset OffsetDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
ValidOffset (SizeExpr' r f)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax

classclass TruncateOffset a where

Make offsets non-negative by rounding up.

Methods

truncateOffset :: a -> a

Instances2TruncateOffset

TruncateOffset OffsetDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
TruncateOffset (SizeExpr' r f)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax

Computing variable sets

7 declarations

classclass Ord (RigidOf a) => Rigids a where

The rigid variables contained in a pice of syntax.

Associated types

type family RigidOf a

Methods

rigids :: a -> Set (RigidOf a)

Instances3Rigids

Rigids a => Rigids [a]Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Ord r => Rigids (Constraint' r f)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Ord r => Rigids (SizeExpr' r f)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax

classclass Ord (FlexOf a) => Flexs a where

The flexibe variables contained in a pice of syntax.

Associated types

type family FlexOf a

Methods

flexs :: a -> Set (FlexOf a)

Instances4Flexs

Flexs HypSizeConstraintDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Flexs a => Flexs [a]Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Ord flex => Flexs (Constraint' rigid flex)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Ord flex => Flexs (SizeExpr' rigid flex)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax

datadata NamedRigid

Identifiers for rigid variables.

Constructors

NamedRigid
- rigidName :: String
  Name for printing in debug messages.
- rigidIndex :: Int
  De Bruijn index.

Instances13Eq, Ord, Show, Generic, NFData, Pretty, …

Eq NamedRigidDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Ord NamedRigidDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Show NamedRigidDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Generic NamedRigidDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
NFData NamedRigidDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Pretty NamedRigidDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Subst SizeConstraintDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Solve · orphan
PrettyTCM SizeConstraintDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Pretty · orphan
Assumes we are in the right context.
Plus NamedRigid Int NamedRigidDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Subst (SizeExpr' NamedRigid SizeMeta)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Solve · orphan
Only for raise.
type Rep NamedRigid = D1 ('MetaData "NamedRigid" "Agda.TypeChecking.SizedTypes.Syntax" "Agda-2.7.0.1-DbbZpETDDF1KkwuzEZvfn8" 'False) (C1 ('MetaCons "NamedRigid" 'PrefixI 'True) (S1 ('MetaSel ('Just "rigidName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Just "rigidIndex") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)))Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
type SubstArg SizeConstraint = TermDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Solve · orphan
type SubstArg (SizeExpr' NamedRigid SizeMeta) = TermDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Solve · orphan

datadata SizeMeta

Size metas in size expressions.

Constructors

SizeMeta
- sizeMetaId :: MetaId
- sizeMetaArgs :: [Int]
  De Bruijn indices.

Instances15Eq, Ord, Show, Generic, NFData, Pretty, …

Eq SizeMetaDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
An equality which ignores the meta arguments.
Ord SizeMetaDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
An order which ignores the meta arguments.
Show SizeMetaDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Generic SizeMetaDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
NFData SizeMetaDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Pretty SizeMetaDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Subst SizeConstraintDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Solve · orphan
Subst SizeMetaDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Solve · orphan
PrettyTCM SizeConstraintDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Pretty · orphan
Assumes we are in the right context.
PrettyTCM SizeMetaDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Pretty · orphan
Subst (SizeExpr' NamedRigid SizeMeta)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Solve · orphan
Only for raise.
type Rep SizeMeta = D1 ('MetaData "SizeMeta" "Agda.TypeChecking.SizedTypes.Syntax" "Agda-2.7.0.1-DbbZpETDDF1KkwuzEZvfn8" 'False) (C1 ('MetaCons "SizeMeta" 'PrefixI 'True) (S1 ('MetaSel ('Just "sizeMetaId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MetaId) :*: S1 ('MetaSel ('Just "sizeMetaArgs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Int])))Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
type SubstArg SizeConstraint = TermDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Solve · orphan
type SubstArg SizeMeta = TermDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Solve · orphan
type SubstArg (SizeExpr' NamedRigid SizeMeta) = TermDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Solve · orphan

typetype DBSizeExpr = SizeExpr' NamedRigid SizeMeta

Size expression with de Bruijn indices.

typetype SizeConstraint = Constraint' NamedRigid SizeMeta

datadata HypSizeConstraint

Size constraint with de Bruijn indices.

Constructors

HypSizeConstraint
- sizeContext :: Context
- sizeHypIds :: [Nat]
  DeBruijn indices
- sizeHypotheses :: [SizeConstraint]
  Living in Context.
- sizeConstraint :: SizeConstraint
  Living in Context.

Instances7Show, Generic, NFData, PrettyTCM, Flexs, Rep, …

Show HypSizeConstraintDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
Generic HypSizeConstraintDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
NFData HypSizeConstraintDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
PrettyTCM HypSizeConstraintDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Pretty · orphan
Flexs HypSizeConstraintDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
type Rep HypSizeConstraint = D1 ('MetaData "HypSizeConstraint" "Agda.TypeChecking.SizedTypes.Syntax" "Agda-2.7.0.1-DbbZpETDDF1KkwuzEZvfn8" 'False) (C1 ('MetaCons "HypSizeConstraint" 'PrefixI 'True) ((S1 ('MetaSel ('Just "sizeContext") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Context) :*: S1 ('MetaSel ('Just "sizeHypIds") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Nat])) :*: (S1 ('MetaSel ('Just "sizeHypotheses") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SizeConstraint]) :*: S1 ('MetaSel ('Just "sizeConstraint") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SizeConstraint))))Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
type FlexOf HypSizeConstraint = SizeMetaDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax