ModuleAgda-2.8.0.2Haskell2010

Agda.TypeChecking.SizedTypes.Syntax

Syntax of size expressions and constraints.

Contents

Syntax
Polarities to specify solutions.
Solutions.
Constraint simplification
Printing
Wellformedness
Computing variable sets

Synopsis

newtype Offset
newtype Rigid
newtype Flex
data SizeExpr'
type SizeExpr
data Cmp
data Constraint'
type Constraint
data Polarity
data PolarityAssignment
type Polarities
value emptyPolarities
value polaritiesFromAssignments
value getPolarity
newtype Solution
value emptySolution
class Substitute
type CTrans
value simplify1
value ifLe
value compareOffset
class ValidOffset
class TruncateOffset
class Rigids
class Flexs
data NamedRigid
data SizeMeta
type DBSizeExpr
type SizeConstraint
data HypSizeConstraint

PackageAgda-2.8.0.2
Exports30
LanguageHaskell2010
LicenceMIT
SourceSyntax.hs

Syntax

newtypenewtype Offset

Source#

Constant finite sizes n >= 0.

Constructors

O Int

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

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

newtypenewtype Rigid

Source#

Fixed size variables i.

Constructors

RigidId
- rigidId :: String

Instances4Eq, Ord, Show, Pretty

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

newtypenewtype Flex

Source#

Size meta variables X to solve for.

Constructors

FlexId
- flexId :: String

Instances4Eq, Ord, Show, Pretty

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

datadata SizeExpr' rigid flex

Source#

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.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
Functor (SizeExpr' rigid)Defined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
Foldable (SizeExpr' rigid)Defined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
Traversable (SizeExpr' rigid)Defined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
(Eq rigid, Eq flex) => Eq (SizeExpr' rigid flex)Defined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
(Ord rigid, Ord flex) => Ord (SizeExpr' rigid flex)Defined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
(Show rigid, Show flex) => Show (SizeExpr' rigid flex)Defined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
Generic (SizeExpr' rigid flex)Defined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
(NFData r, NFData f) => NFData (SizeExpr' r f)Defined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
(Pretty r, Pretty f) => Pretty (SizeExpr' r f)Defined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
Subst (SizeExpr' NamedRigid SizeMeta)Defined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Solve · orphan
Only for raise.
Ord flex => Flexs (SizeExpr' rigid flex)Defined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
Ord r => Rigids (SizeExpr' r f)Defined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
TruncateOffset (SizeExpr' r f)Defined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
ValidOffset (SizeExpr' r f)Defined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
Plus (SizeExpr' r f) Offset (SizeExpr' r f)Defined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
Add offset to size expression.
Plus (SizeExpr' r f) Label (SizeExpr' r f)Defined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.WarshallSolver
Plus (SizeExpr' r f) Weight (SizeExpr' r f)Defined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.WarshallSolver
type Rep (SizeExpr' rigid flex) = D1 ('MetaData "SizeExpr'" "Agda.TypeChecking.SizedTypes.Syntax" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" '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.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
type SubstArg (SizeExpr' NamedRigid SizeMeta) = TermDefined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Solve · orphan
type FlexOf (SizeExpr' rigid flex) = flexDefined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
type RigidOf (SizeExpr' r f) = rDefined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax

typetype SizeExpr = SizeExpr' Rigid Flex

datadata Cmp

Source#

Comparison operator, e.g. for size expression.

Constructors

Lt
<.
Le
≤.

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

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

datadata Constraint' rigid flex

Source#

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.8.0.2 · Agda.TypeChecking.SizedTypes.Solve · orphan
PrettyTCM SizeConstraintDefined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Pretty · orphan
Assumes we are in the right context.
Ord f => Substitute r f (Constraint' r f)Defined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
Functor (Constraint' rigid)Defined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
Foldable (Constraint' rigid)Defined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
Traversable (Constraint' rigid)Defined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
(Show rigid, Show flex) => Show (Constraint' rigid flex)Defined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
Generic (Constraint' rigid flex)Defined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
(NFData r, NFData f) => NFData (Constraint' r f)Defined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
(Pretty r, Pretty f) => Pretty (Constraint' r f)Defined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
Ord flex => Flexs (Constraint' rigid flex)Defined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
Ord r => Rigids (Constraint' r f)Defined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
type Rep (Constraint' rigid flex) = D1 ('MetaData "Constraint'" "Agda.TypeChecking.SizedTypes.Syntax" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" '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.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
type SubstArg SizeConstraint = TermDefined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Solve · orphan
type FlexOf (Constraint' rigid flex) = flexDefined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
type RigidOf (Constraint' r f) = rDefined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax

typetype Constraint = Constraint' Rigid Flex

Polarities to specify solutions.

datadata Polarity

Source#

What type of solution are we looking for?

Least Greatest

Instances3Eq, Ord, Pretty

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

datadata PolarityAssignment flex

Source#

Assigning a polarity to a flexible variable.

Constructors

PolarityAssignment Polarity flex

Instances1Pretty

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

typetype Polarities flex = Map flex Polarity

Source#

Type of solution wanted for each flexible.

valueemptyPolarities :: Polarities flex

valuepolaritiesFromAssignments

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

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

Source#

Default polarity is Least.

Solutions.

newtypenewtype Solution rigid flex

Source#

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.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
(Show flex, Show rigid) => Show (Solution rigid flex)Defined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
(Pretty r, Pretty f) => Pretty (Solution r f)Defined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
Null (Solution rigid flex)Defined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax

valueemptySolution :: Solution r f

classclass Substitute r f a where

Source#

Executing a substitution.

Methods

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

Instances5Substitute

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

Constraint simplification

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

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

Source#

Returns Nothing if the constraint is contradictory.

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

Source#

Le acts as True, Lt as False.

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

Source#

Interpret Cmp as relation on Offset.

Printing

Wellformedness

classclass ValidOffset a where

Source#

Offsets + n must be non-negative

Methods

validOffset :: a -> Bool

Instances2ValidOffset

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

classclass TruncateOffset a where

Source#

Make offsets non-negative by rounding up.

Methods

truncateOffset :: a -> a

Instances2TruncateOffset

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

Computing variable sets

classclass Ord (RigidOf a) => Rigids a where

Source#

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.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
Ord r => Rigids (Constraint' r f)Defined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
Ord r => Rigids (SizeExpr' r f)Defined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax

classclass Ord (FlexOf a) => Flexs a where

Source#

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.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
Flexs a => Flexs [a]Defined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
Ord flex => Flexs (Constraint' rigid flex)Defined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
Ord flex => Flexs (SizeExpr' rigid flex)Defined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax

datadata NamedRigid

Source#

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.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
Ord NamedRigidDefined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
Show NamedRigidDefined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
Generic NamedRigidDefined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
NFData NamedRigidDefined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
Pretty NamedRigidDefined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
Subst SizeConstraintDefined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Solve · orphan
PrettyTCM SizeConstraintDefined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Pretty · orphan
Assumes we are in the right context.
Plus NamedRigid Int NamedRigidDefined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
Subst (SizeExpr' NamedRigid SizeMeta)Defined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Solve · orphan
Only for raise.
type Rep NamedRigid = D1 ('MetaData "NamedRigid" "Agda.TypeChecking.SizedTypes.Syntax" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" '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.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
type SubstArg SizeConstraint = TermDefined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Solve · orphan
type SubstArg (SizeExpr' NamedRigid SizeMeta) = TermDefined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Solve · orphan

datadata SizeMeta

Source#

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.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
An equality which ignores the meta arguments.
Ord SizeMetaDefined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
An order which ignores the meta arguments.
Show SizeMetaDefined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
Generic SizeMetaDefined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
NFData SizeMetaDefined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
Pretty SizeMetaDefined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
Subst SizeConstraintDefined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Solve · orphan
Subst SizeMetaDefined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Solve · orphan
PrettyTCM SizeConstraintDefined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Pretty · orphan
Assumes we are in the right context.
PrettyTCM SizeMetaDefined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Pretty · orphan
Subst (SizeExpr' NamedRigid SizeMeta)Defined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Solve · orphan
Only for raise.
type Rep SizeMeta = D1 ('MetaData "SizeMeta" "Agda.TypeChecking.SizedTypes.Syntax" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" '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.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
type SubstArg SizeConstraint = TermDefined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Solve · orphan
type SubstArg SizeMeta = TermDefined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Solve · orphan
type SubstArg (SizeExpr' NamedRigid SizeMeta) = TermDefined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Solve · orphan

typetype DBSizeExpr = SizeExpr' NamedRigid SizeMeta

Source#

Size expression with de Bruijn indices.

typetype SizeConstraint = Constraint' NamedRigid SizeMeta

datadata HypSizeConstraint

Source#

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.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
Generic HypSizeConstraintDefined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
NFData HypSizeConstraintDefined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
PrettyTCM HypSizeConstraintDefined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Pretty · orphan
Flexs HypSizeConstraintDefined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
type Rep HypSizeConstraint = D1 ('MetaData "HypSizeConstraint" "Agda.TypeChecking.SizedTypes.Syntax" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" '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.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
type FlexOf HypSizeConstraint = SizeMetaDefined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax