Agda-2.6.4: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.TypeChecking.SizedTypes.Syntax

Description

Syntax of size expressions and constraints.

Synopsis

Syntax

newtype Offset Source #

Constant finite sizes n >= 0.

Constructors

O Int 

Instances

Instances details
Pretty Offset Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

TruncateOffset Offset Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

ValidOffset Offset Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

validOffset :: Offset -> Bool Source #

MeetSemiLattice Offset Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

meet :: Offset -> Offset -> Offset Source #

Negative Offset Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

negative :: Offset -> Bool Source #

Enum Offset Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Num Offset Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Show Offset Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

showsPrec :: Int -> Offset -> ShowS

show :: Offset -> String

showList :: [Offset] -> ShowS

Eq Offset Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

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

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

Ord Offset Source # 
Instance details

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 Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

plus :: Offset -> Offset -> Offset Source #

Plus Offset Weight Weight Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

plus :: Offset -> Weight -> Weight Source #

Plus Weight Offset Weight Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

plus :: Weight -> Offset -> Weight Source #

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

Add offset to size expression.

Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

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

newtype Rigid Source #

Fixed size variables i.

Constructors

RigidId 

Fields

Instances

Instances details
Pretty Rigid Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Show Rigid Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

showsPrec :: Int -> Rigid -> ShowS

show :: Rigid -> String

showList :: [Rigid] -> ShowS

Eq Rigid Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

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

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

Ord Rigid Source # 
Instance details

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 Source #

Size meta variables X to solve for.

Constructors

FlexId 

Fields

Instances

Instances details
Pretty Flex Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

pretty :: Flex -> Doc Source #

prettyPrec :: Int -> Flex -> Doc Source #

prettyList :: [Flex] -> Doc Source #

PrettyTCM Flex Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

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

Show Flex Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

showsPrec :: Int -> Flex -> ShowS

show :: Flex -> String

showList :: [Flex] -> ShowS

Eq Flex Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

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

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

Ord Flex Source # 
Instance details

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 Source #

Size expressions appearing in constraints.

Constructors

Const

Constant number n.

Fields

Rigid

Variable plus offset i + n.

Fields

Infty

Infinity .

Flex

Meta variable X + n.

Fields

Instances

Instances details
Ord f => Substitute r f (SizeExpr' r f) Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

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

Foldable (SizeExpr' rigid) Source # 
Instance details

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) Source # 
Instance details

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) Source # 
Instance details

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) Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

pretty :: SizeExpr' r f -> Doc Source #

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

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

Ord flex => Flexs (SizeExpr' rigid flex) Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Associated Types

type FlexOf (SizeExpr' rigid flex) Source #

Methods

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

Ord r => Rigids (SizeExpr' r f) Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Associated Types

type RigidOf (SizeExpr' r f) Source #

Methods

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

TruncateOffset (SizeExpr' r f) Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

ValidOffset (SizeExpr' r f) Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

validOffset :: SizeExpr' r f -> Bool Source #

Subst (SizeExpr' NamedRigid SizeMeta) Source #

Only for raise.

Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

Associated Types

type SubstArg (SizeExpr' NamedRigid SizeMeta) Source #

(Show rigid, Show flex) => Show (SizeExpr' rigid flex) Source # 
Instance details

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) Source # 
Instance details

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) Source # 
Instance details

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) Source #

Add offset to size expression.

Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

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

Plus (SizeExpr' r f) Label (SizeExpr' r f) Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

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

Plus (SizeExpr' r f) Weight (SizeExpr' r f) Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

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

type FlexOf (SizeExpr' rigid flex) Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

type FlexOf (SizeExpr' rigid flex) = flex
type RigidOf (SizeExpr' r f) Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

type RigidOf (SizeExpr' r f) = r
type SubstArg (SizeExpr' NamedRigid SizeMeta) Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

data Cmp Source #

Comparison operator, e.g. for size expression.

Constructors

Lt

<.

Le

.

Instances

Instances details
Pretty Cmp Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

pretty :: Cmp -> Doc Source #

prettyPrec :: Int -> Cmp -> Doc Source #

prettyList :: [Cmp] -> Doc Source #

Dioid Cmp Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

MeetSemiLattice Cmp Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

meet :: Cmp -> Cmp -> Cmp Source #

Top Cmp Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

top :: Cmp Source #

isTop :: Cmp -> Bool Source #

Bounded Cmp Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

minBound :: Cmp

maxBound :: Cmp

Enum Cmp Source # 
Instance details

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 Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

showsPrec :: Int -> Cmp -> ShowS

show :: Cmp -> String

showList :: [Cmp] -> ShowS

Eq Cmp Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

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

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

Ord Cmp Source #

Comparison operator is ordered Lt < Le.

Instance details

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 Source #

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

Constructors

Constraint 

Fields

Instances

Instances details
PrettyTCM SizeConstraint Source #

Assumes we are in the right context.

Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

Subst SizeConstraint Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

Associated Types

type SubstArg SizeConstraint Source #

Ord f => Substitute r f (Constraint' r f) Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

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

Foldable (Constraint' rigid) Source # 
Instance details

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) Source # 
Instance details

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) Source # 
Instance details

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) Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Ord flex => Flexs (Constraint' rigid flex) Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Associated Types

type FlexOf (Constraint' rigid flex) Source #

Methods

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

Ord r => Rigids (Constraint' r f) Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Associated Types

type RigidOf (Constraint' r f) Source #

Methods

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

(Show rigid, Show flex) => Show (Constraint' rigid flex) Source # 
Instance details

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 Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

type FlexOf (Constraint' rigid flex) Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

type FlexOf (Constraint' rigid flex) = flex
type RigidOf (Constraint' r f) Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

type RigidOf (Constraint' r f) = r

Polarities to specify solutions.

data Polarity Source #

What type of solution are we looking for?

Constructors

Least 
Greatest 

Instances

Instances details
Pretty Polarity Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Eq Polarity Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

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

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

Ord Polarity Source # 
Instance details

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 Source #

Assigning a polarity to a flexible variable.

Constructors

PolarityAssignment Polarity flex 

Instances

Instances details
Pretty flex => Pretty (PolarityAssignment flex) Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

type Polarities flex = Map flex Polarity Source #

Type of solution wanted for each flexible.

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

Default polarity is Least.

Solutions.

newtype Solution rigid flex Source #

Partial substitution from flexible variables to size expression.

Constructors

Solution 

Fields

Instances

Instances details
Ord f => Substitute r f (Solution r f) Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

subst :: Solution r f -> Solution r f -> Solution r f Source #

(Pretty r, Pretty f) => Pretty (Solution r f) Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

pretty :: Solution r f -> Doc Source #

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

prettyList :: [Solution r f] -> Doc Source #

Null (Solution rigid flex) Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

empty :: Solution rigid flex Source #

null :: Solution rigid flex -> Bool Source #

(Show flex, Show rigid) => Show (Solution rigid flex) Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

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

show :: Solution rigid flex -> String

showList :: [Solution rigid flex] -> ShowS

class Substitute r f a where Source #

Executing a substitution.

Methods

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

Instances

Instances details
Substitute r f a => Substitute r f [a] Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

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

Ord f => Substitute r f (Constraint' r f) Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

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

Ord f => Substitute r f (SizeExpr' r f) Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

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

Ord f => Substitute r f (Solution r f) Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

subst :: Solution r f -> Solution r f -> Solution r f Source #

Substitute r f a => Substitute r f (Map k a) Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

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

type Error = TCM Doc Source #

Error messages produced by the constraint simplification monad.

Constraint simplification

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

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

Returns an error message if we have a contradictory constraint.

ifLe :: Cmp -> a -> a -> a Source #

Le acts as True, Lt as False.

compareOffset :: Offset -> Cmp -> Offset -> Bool Source #

Interpret Cmp as relation on Offset.

Printing

Wellformedness

class ValidOffset a where Source #

Offsets + n must be non-negative

Methods

validOffset :: a -> Bool Source #

Instances

Instances details
ValidOffset Offset Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

validOffset :: Offset -> Bool Source #

ValidOffset (SizeExpr' r f) Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

validOffset :: SizeExpr' r f -> Bool Source #

class TruncateOffset a where Source #

Make offsets non-negative by rounding up.

Methods

truncateOffset :: a -> a Source #

Instances

Instances details
TruncateOffset Offset Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

TruncateOffset (SizeExpr' r f) Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Computing variable sets

class Ord (RigidOf a) => Rigids a where Source #

The rigid variables contained in a pice of syntax.

Associated Types

type RigidOf a Source #

Methods

rigids :: a -> Set (RigidOf a) Source #

Instances

Instances details
Rigids a => Rigids [a] Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Associated Types

type RigidOf [a] Source #

Methods

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

Ord r => Rigids (Constraint' r f) Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Associated Types

type RigidOf (Constraint' r f) Source #

Methods

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

Ord r => Rigids (SizeExpr' r f) Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Associated Types

type RigidOf (SizeExpr' r f) Source #

Methods

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

class Ord (FlexOf a) => Flexs a where Source #

The flexibe variables contained in a pice of syntax.

Associated Types

type FlexOf a Source #

Methods

flexs :: a -> Set (FlexOf a) Source #

Instances

Instances details
Flexs HypSizeConstraint Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

Associated Types

type FlexOf HypSizeConstraint Source #

Flexs a => Flexs [a] Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Associated Types

type FlexOf [a] Source #

Methods

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

Ord flex => Flexs (Constraint' rigid flex) Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Associated Types

type FlexOf (Constraint' rigid flex) Source #

Methods

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

Ord flex => Flexs (SizeExpr' rigid flex) Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Associated Types

type FlexOf (SizeExpr' rigid flex) Source #

Methods

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