Agda.TypeChecking.SizedTypes.Syntax

Syntax of size expressions and constraints.

Syntax

newtype Offset

Constant finite sizes n >= 0.

Constructors

O Int

Instances

Pretty Offset

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

pretty :: Offset -> Doc

prettyPrec :: Int -> Offset -> Doc

prettyList :: [Offset] -> Doc

TruncateOffset Offset

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

truncateOffset :: Offset -> Offset

ValidOffset Offset

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

validOffset :: Offset -> Bool

MeetSemiLattice Offset

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

meet :: Offset -> Offset -> Offset

Negative Offset

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

negative :: Offset -> Bool

Enum Offset

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

succ :: Offset -> Offset

pred :: Offset -> Offset

toEnum :: Int -> Offset

fromEnum :: Offset -> Int

enumFrom :: Offset -> [Offset]

enumFromThen :: Offset -> Offset -> [Offset]

enumFromTo :: Offset -> Offset -> [Offset]

enumFromThenTo :: Offset -> Offset -> Offset -> [Offset]

Num Offset

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

(+) :: Offset -> Offset -> Offset

(-) :: Offset -> Offset -> Offset

(*) :: Offset -> Offset -> Offset

negate :: Offset -> Offset

abs :: Offset -> Offset

signum :: Offset -> Offset

fromInteger :: Integer -> Offset

Show Offset

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

showsPrec :: Int -> Offset -> ShowS

show :: Offset -> String

showList :: [Offset] -> ShowS

Eq Offset

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

(==) :: Offset -> Offset -> Bool

(/=) :: Offset -> Offset -> Bool

Ord Offset

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

compare :: Offset -> Offset -> Ordering

(<) :: Offset -> Offset -> Bool

(<=) :: Offset -> Offset -> Bool

(>) :: Offset -> Offset -> Bool

(>=) :: Offset -> Offset -> Bool

max :: Offset -> Offset -> Offset

min :: Offset -> Offset -> Offset

Plus Offset Offset Offset

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

plus :: Offset -> Offset -> Offset

Plus Offset Weight Weight

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

plus :: Offset -> Weight -> Weight

Plus Weight Offset Weight

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

plus :: Weight -> Offset -> Weight

Plus (SizeExpr' r f) Offset (SizeExpr' r f)

Add offset to size expression.

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

plus :: SizeExpr' r f -> Offset -> SizeExpr' r f

newtype Rigid

Fixed size variables i.

Constructors

RigidId

Fields

• rigidId :: String

Instances

Pretty Rigid

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

pretty :: Rigid -> Doc

prettyPrec :: Int -> Rigid -> Doc

prettyList :: [Rigid] -> Doc

Show Rigid

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

showsPrec :: Int -> Rigid -> ShowS

show :: Rigid -> String

showList :: [Rigid] -> ShowS

Eq Rigid

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

(==) :: Rigid -> Rigid -> Bool

(/=) :: Rigid -> Rigid -> Bool

Ord Rigid

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

compare :: Rigid -> Rigid -> Ordering

(<) :: Rigid -> Rigid -> Bool

(<=) :: Rigid -> Rigid -> Bool

(>) :: Rigid -> Rigid -> Bool

(>=) :: Rigid -> Rigid -> Bool

max :: Rigid -> Rigid -> Rigid

min :: Rigid -> Rigid -> Rigid

newtype Flex

Size meta variables X to solve for.

Constructors

FlexId

Fields

• flexId :: String

Instances

Pretty Flex

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

pretty :: Flex -> Doc

prettyPrec :: Int -> Flex -> Doc

prettyList :: [Flex] -> Doc

PrettyTCM Flex

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

prettyTCM :: MonadPretty m => Flex -> m Doc

Show Flex

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

showsPrec :: Int -> Flex -> ShowS

show :: Flex -> String

showList :: [Flex] -> ShowS

Eq Flex

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

(==) :: Flex -> Flex -> Bool

(/=) :: Flex -> Flex -> Bool

Ord Flex

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

compare :: Flex -> Flex -> Ordering

(<) :: Flex -> Flex -> Bool

(<=) :: Flex -> Flex -> Bool

(>) :: Flex -> Flex -> Bool

(>=) :: Flex -> Flex -> Bool

max :: Flex -> Flex -> Flex

min :: Flex -> Flex -> Flex

data SizeExpr' rigid flex

Size expressions appearing in constraints.

Constructors

Const

Constant number n.

Fields

• offset :: Offset

Rigid

Variable plus offset i + n.

Fields

• rigid :: rigid
• offset :: Offset

Infty

Infinity ∞.

Flex

Meta variable X + n.

Fields

• flex :: flex
• offset :: Offset

Instances

Ord f => Substitute r f (SizeExpr' r f)

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

subst :: Solution r f -> SizeExpr' r f -> SizeExpr' r f

Foldable (SizeExpr' rigid)

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

fold :: Monoid m => SizeExpr' rigid m -> m

foldMap :: Monoid m => (a -> m) -> SizeExpr' rigid a -> m

foldMap' :: Monoid m => (a -> m) -> SizeExpr' rigid a -> m

foldr :: (a -> b -> b) -> b -> SizeExpr' rigid a -> b

foldr' :: (a -> b -> b) -> b -> SizeExpr' rigid a -> b

foldl :: (b -> a -> b) -> b -> SizeExpr' rigid a -> b

foldl' :: (b -> a -> b) -> b -> SizeExpr' rigid a -> b

foldr1 :: (a -> a -> a) -> SizeExpr' rigid a -> a

foldl1 :: (a -> a -> a) -> SizeExpr' rigid a -> a

toList :: SizeExpr' rigid a -> [a]

null :: SizeExpr' rigid a -> Bool

length :: SizeExpr' rigid a -> Int

elem :: Eq a => a -> SizeExpr' rigid a -> Bool

maximum :: Ord a => SizeExpr' rigid a -> a

minimum :: Ord a => SizeExpr' rigid a -> a

sum :: Num a => SizeExpr' rigid a -> a

product :: Num a => SizeExpr' rigid a -> a

Traversable (SizeExpr' rigid)

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

traverse :: Applicative f => (a -> f b) -> SizeExpr' rigid a -> f (SizeExpr' rigid b)

sequenceA :: Applicative f => SizeExpr' rigid (f a) -> f (SizeExpr' rigid a)

mapM :: Monad m => (a -> m b) -> SizeExpr' rigid a -> m (SizeExpr' rigid b)

sequence :: Monad m => SizeExpr' rigid (m a) -> m (SizeExpr' rigid a)

Functor (SizeExpr' rigid)

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

fmap :: (a -> b) -> SizeExpr' rigid a -> SizeExpr' rigid b

(<$) :: a -> SizeExpr' rigid b -> SizeExpr' rigid a

(Pretty r, Pretty f) => Pretty (SizeExpr' r f)

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

pretty :: SizeExpr' r f -> Doc

prettyPrec :: Int -> SizeExpr' r f -> Doc

prettyList :: [SizeExpr' r f] -> Doc

Ord flex => Flexs (SizeExpr' rigid flex)

Defined in Agda.TypeChecking.SizedTypes.Syntax

Associated Types

type FlexOf (SizeExpr' rigid flex)

Methods

flexs :: SizeExpr' rigid flex -> Set (FlexOf (SizeExpr' rigid flex))

Ord r => Rigids (SizeExpr' r f)

Defined in Agda.TypeChecking.SizedTypes.Syntax

Associated Types

type RigidOf (SizeExpr' r f)

Methods

rigids :: SizeExpr' r f -> Set (RigidOf (SizeExpr' r f))

TruncateOffset (SizeExpr' r f)

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

truncateOffset :: SizeExpr' r f -> SizeExpr' r f

ValidOffset (SizeExpr' r f)

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

validOffset :: SizeExpr' r f -> Bool

Subst (SizeExpr' NamedRigid SizeMeta)

Only for raise.

Defined in Agda.TypeChecking.SizedTypes.Solve

Associated Types

type SubstArg (SizeExpr' NamedRigid SizeMeta)

Methods

applySubst :: Substitution' (SubstArg (SizeExpr' NamedRigid SizeMeta)) -> SizeExpr' NamedRigid SizeMeta -> SizeExpr' NamedRigid SizeMeta

(Show rigid, Show flex) => Show (SizeExpr' rigid flex)

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

showsPrec :: Int -> SizeExpr' rigid flex -> ShowS

show :: SizeExpr' rigid flex -> String

showList :: [SizeExpr' rigid flex] -> ShowS

(Eq rigid, Eq flex) => Eq (SizeExpr' rigid flex)

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

(==) :: SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool

(/=) :: SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool

(Ord rigid, Ord flex) => Ord (SizeExpr' rigid flex)

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

compare :: SizeExpr' rigid flex -> SizeExpr' rigid flex -> Ordering

(<) :: SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool

(<=) :: SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool

(>) :: SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool

(>=) :: SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool

max :: SizeExpr' rigid flex -> SizeExpr' rigid flex -> SizeExpr' rigid flex

min :: SizeExpr' rigid flex -> SizeExpr' rigid flex -> SizeExpr' rigid flex

Plus (SizeExpr' r f) Offset (SizeExpr' r f)

Add offset to size expression.

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

plus :: SizeExpr' r f -> Offset -> SizeExpr' r f

Plus (SizeExpr' r f) Label (SizeExpr' r f)

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

plus :: SizeExpr' r f -> Label -> SizeExpr' r f

Plus (SizeExpr' r f) Weight (SizeExpr' r f)

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

plus :: SizeExpr' r f -> Weight -> SizeExpr' r f

type FlexOf (SizeExpr' rigid flex)

Defined in Agda.TypeChecking.SizedTypes.Syntax

type FlexOf (SizeExpr' rigid flex) = flex

type RigidOf (SizeExpr' r f)

Defined in Agda.TypeChecking.SizedTypes.Syntax

type RigidOf (SizeExpr' r f) = r

type SubstArg (SizeExpr' NamedRigid SizeMeta)

Defined in Agda.TypeChecking.SizedTypes.Solve

type SubstArg (SizeExpr' NamedRigid SizeMeta) = Term

type SizeExpr = SizeExpr' Rigid Flex

data Cmp

Comparison operator, e.g. for size expression.

Constructors

Lt

<.

Le

≤.

Instances

Pretty Cmp

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

pretty :: Cmp -> Doc

prettyPrec :: Int -> Cmp -> Doc

prettyList :: [Cmp] -> Doc

Dioid Cmp

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

compose :: Cmp -> Cmp -> Cmp

unitCompose :: Cmp

MeetSemiLattice Cmp

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

meet :: Cmp -> Cmp -> Cmp

Top Cmp

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

top :: Cmp

isTop :: Cmp -> Bool

Bounded Cmp

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

minBound :: Cmp

maxBound :: Cmp

Enum Cmp

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

succ :: Cmp -> Cmp

pred :: Cmp -> Cmp

toEnum :: Int -> Cmp

fromEnum :: Cmp -> Int

enumFrom :: Cmp -> [Cmp]

enumFromThen :: Cmp -> Cmp -> [Cmp]

enumFromTo :: Cmp -> Cmp -> [Cmp]

enumFromThenTo :: Cmp -> Cmp -> Cmp -> [Cmp]

Show Cmp

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

showsPrec :: Int -> Cmp -> ShowS

show :: Cmp -> String

showList :: [Cmp] -> ShowS

Eq Cmp

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

(==) :: Cmp -> Cmp -> Bool

(/=) :: Cmp -> Cmp -> Bool

Ord Cmp

Comparison operator is ordered Lt < Le.

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

compare :: Cmp -> Cmp -> Ordering

(<) :: Cmp -> Cmp -> Bool

(<=) :: Cmp -> Cmp -> Bool

(>) :: Cmp -> Cmp -> Bool

(>=) :: Cmp -> Cmp -> Bool

max :: Cmp -> Cmp -> Cmp

min :: Cmp -> Cmp -> Cmp

data Constraint' rigid flex

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

Constructors

Constraint

Fields

• leftExpr :: SizeExpr' rigid flex
• cmp :: Cmp
• rightExpr :: SizeExpr' rigid flex

Instances

PrettyTCM SizeConstraint

Assumes we are in the right context.

Defined in Agda.TypeChecking.SizedTypes.Solve

Methods

prettyTCM :: MonadPretty m => SizeConstraint -> m Doc

Subst SizeConstraint

Defined in Agda.TypeChecking.SizedTypes.Solve

Associated Types

type SubstArg SizeConstraint

Methods

applySubst :: Substitution' (SubstArg SizeConstraint) -> SizeConstraint -> SizeConstraint

Ord f => Substitute r f (Constraint' r f)

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

subst :: Solution r f -> Constraint' r f -> Constraint' r f

Foldable (Constraint' rigid)

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

fold :: Monoid m => Constraint' rigid m -> m

foldMap :: Monoid m => (a -> m) -> Constraint' rigid a -> m

foldMap' :: Monoid m => (a -> m) -> Constraint' rigid a -> m

foldr :: (a -> b -> b) -> b -> Constraint' rigid a -> b

foldr' :: (a -> b -> b) -> b -> Constraint' rigid a -> b

foldl :: (b -> a -> b) -> b -> Constraint' rigid a -> b

foldl' :: (b -> a -> b) -> b -> Constraint' rigid a -> b

foldr1 :: (a -> a -> a) -> Constraint' rigid a -> a

foldl1 :: (a -> a -> a) -> Constraint' rigid a -> a

toList :: Constraint' rigid a -> [a]

null :: Constraint' rigid a -> Bool

length :: Constraint' rigid a -> Int

elem :: Eq a => a -> Constraint' rigid a -> Bool

maximum :: Ord a => Constraint' rigid a -> a

minimum :: Ord a => Constraint' rigid a -> a

sum :: Num a => Constraint' rigid a -> a

product :: Num a => Constraint' rigid a -> a

Traversable (Constraint' rigid)

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

traverse :: Applicative f => (a -> f b) -> Constraint' rigid a -> f (Constraint' rigid b)

sequenceA :: Applicative f => Constraint' rigid (f a) -> f (Constraint' rigid a)

mapM :: Monad m => (a -> m b) -> Constraint' rigid a -> m (Constraint' rigid b)

sequence :: Monad m => Constraint' rigid (m a) -> m (Constraint' rigid a)

Functor (Constraint' rigid)

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

fmap :: (a -> b) -> Constraint' rigid a -> Constraint' rigid b

(<$) :: a -> Constraint' rigid b -> Constraint' rigid a

(Pretty r, Pretty f) => Pretty (Constraint' r f)

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

pretty :: Constraint' r f -> Doc

prettyPrec :: Int -> Constraint' r f -> Doc

prettyList :: [Constraint' r f] -> Doc

Ord flex => Flexs (Constraint' rigid flex)

Defined in Agda.TypeChecking.SizedTypes.Syntax

Associated Types

type FlexOf (Constraint' rigid flex)

Methods

flexs :: Constraint' rigid flex -> Set (FlexOf (Constraint' rigid flex))

Ord r => Rigids (Constraint' r f)

Defined in Agda.TypeChecking.SizedTypes.Syntax

Associated Types

type RigidOf (Constraint' r f)

Methods

rigids :: Constraint' r f -> Set (RigidOf (Constraint' r f))

(Show rigid, Show flex) => Show (Constraint' rigid flex)

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

showsPrec :: Int -> Constraint' rigid flex -> ShowS

show :: Constraint' rigid flex -> String

showList :: [Constraint' rigid flex] -> ShowS

type SubstArg SizeConstraint

Defined in Agda.TypeChecking.SizedTypes.Solve

type SubstArg SizeConstraint = Term

type FlexOf (Constraint' rigid flex)

Defined in Agda.TypeChecking.SizedTypes.Syntax

type FlexOf (Constraint' rigid flex) = flex

type RigidOf (Constraint' r f)

Defined in Agda.TypeChecking.SizedTypes.Syntax

type RigidOf (Constraint' r f) = r

type Constraint = Constraint' Rigid Flex

Polarities to specify solutions.

data Polarity

What type of solution are we looking for?

Constructors

Least

Greatest

Instances

Pretty Polarity

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

pretty :: Polarity -> Doc

prettyPrec :: Int -> Polarity -> Doc

prettyList :: [Polarity] -> Doc

Eq Polarity

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

(==) :: Polarity -> Polarity -> Bool

(/=) :: Polarity -> Polarity -> Bool

Ord Polarity

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

compare :: Polarity -> Polarity -> Ordering

(<) :: Polarity -> Polarity -> Bool

(<=) :: Polarity -> Polarity -> Bool

(>) :: Polarity -> Polarity -> Bool

(>=) :: Polarity -> Polarity -> Bool

max :: Polarity -> Polarity -> Polarity

min :: Polarity -> Polarity -> Polarity

data PolarityAssignment flex

Assigning a polarity to a flexible variable.

Constructors

PolarityAssignment Polarity flex

Instances

Pretty flex => Pretty (PolarityAssignment flex)

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

pretty :: PolarityAssignment flex -> Doc

prettyPrec :: Int -> PolarityAssignment flex -> Doc

prettyList :: [PolarityAssignment flex] -> Doc

type Polarities flex = Map flex Polarity

Type of solution wanted for each flexible.

emptyPolarities :: Polarities flex

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

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

Default polarity is Least.

Solutions.

newtype Solution rigid flex

Partial substitution from flexible variables to size expression.

Constructors

Solution

Fields

• theSolution :: Map flex (SizeExpr' rigid flex)

Instances

Ord f => Substitute r f (Solution r f)

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

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

(Pretty r, Pretty f) => Pretty (Solution r f)

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

pretty :: Solution r f -> Doc

prettyPrec :: Int -> Solution r f -> Doc

prettyList :: [Solution r f] -> Doc

Null (Solution rigid flex)

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

empty :: Solution rigid flex

null :: Solution rigid flex -> Bool

(Show flex, Show rigid) => Show (Solution rigid flex)

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

showsPrec :: Int -> Solution rigid flex -> ShowS

show :: Solution rigid flex -> String

showList :: [Solution rigid flex] -> ShowS

emptySolution :: Solution r f

class Substitute r f a where

Executing a substitution.

Methods

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

Instances

Substitute r f a => Substitute r f [a]

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

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

Ord f => Substitute r f (Constraint' r f)

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

subst :: Solution r f -> Constraint' r f -> Constraint' r f

Ord f => Substitute r f (SizeExpr' r f)

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

subst :: Solution r f -> SizeExpr' r f -> SizeExpr' r f

Ord f => Substitute r f (Solution r f)

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

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

Substitute r f a => Substitute r f (Map k a)

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

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

type Error = TCM Doc

Error messages produced by the constraint simplification monad.

Constraint simplification

type CTrans r f = Constraint' r f -> Either Error [Constraint' r f]

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

Returns an error message if we have a contradictory constraint.

ifLe :: Cmp -> a -> a -> a

Le acts as True, Lt as False.

compareOffset :: Offset -> Cmp -> Offset -> Bool

Interpret Cmp as relation on Offset.

Printing

Wellformedness

class ValidOffset a where

Offsets + n must be non-negative

Methods

validOffset :: a -> Bool

Instances

ValidOffset Offset

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

validOffset :: Offset -> Bool

ValidOffset (SizeExpr' r f)

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

validOffset :: SizeExpr' r f -> Bool

class TruncateOffset a where

Make offsets non-negative by rounding up.

Methods

truncateOffset :: a -> a

Instances

TruncateOffset Offset

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

truncateOffset :: Offset -> Offset

TruncateOffset (SizeExpr' r f)

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

truncateOffset :: SizeExpr' r f -> SizeExpr' r f

Computing variable sets

class Ord (RigidOf a) => Rigids a where

The rigid variables contained in a pice of syntax.

Associated Types

type RigidOf a

Methods

rigids :: a -> Set (RigidOf a)

Instances

Rigids a => Rigids [a]

Defined in Agda.TypeChecking.SizedTypes.Syntax

Associated Types

type RigidOf [a]

Methods

rigids :: [a] -> Set (RigidOf [a])

Ord r => Rigids (Constraint' r f)

Defined in Agda.TypeChecking.SizedTypes.Syntax

Associated Types

type RigidOf (Constraint' r f)

Methods

rigids :: Constraint' r f -> Set (RigidOf (Constraint' r f))

Ord r => Rigids (SizeExpr' r f)

Defined in Agda.TypeChecking.SizedTypes.Syntax

Associated Types

type RigidOf (SizeExpr' r f)

Methods

rigids :: SizeExpr' r f -> Set (RigidOf (SizeExpr' r f))

class Ord (FlexOf a) => Flexs a where

The flexibe variables contained in a pice of syntax.

Associated Types

type FlexOf a

Methods

flexs :: a -> Set (FlexOf a)

Instances

Flexs HypSizeConstraint

Defined in Agda.TypeChecking.SizedTypes.Solve

Associated Types

type FlexOf HypSizeConstraint

Methods

flexs :: HypSizeConstraint -> Set (FlexOf HypSizeConstraint)

Flexs a => Flexs [a]

Defined in Agda.TypeChecking.SizedTypes.Syntax

Associated Types

type FlexOf [a]

Methods

flexs :: [a] -> Set (FlexOf [a])

Ord flex => Flexs (Constraint' rigid flex)

Defined in Agda.TypeChecking.SizedTypes.Syntax

Associated Types

type FlexOf (Constraint' rigid flex)

Methods

flexs :: Constraint' rigid flex -> Set (FlexOf (Constraint' rigid flex))

Ord flex => Flexs (SizeExpr' rigid flex)

Defined in Agda.TypeChecking.SizedTypes.Syntax

Associated Types

type FlexOf (SizeExpr' rigid flex)

Methods

flexs :: SizeExpr' rigid flex -> Set (FlexOf (SizeExpr' rigid flex))