Agda.TypeChecking.SizedTypes.Syntax

Syntax

data Offset

data Rigid

data Flex

data SizeExpr' rigid flex

type SizeExpr

data Cmp

data Constraint' rigid flex

type Constraint

Polarities to specify solutions.

data Polarity

data PolarityAssignment flex

type Polarities flex

emptyPolarities

polaritiesFromAssignments

getPolarity

Solutions.

type Solution rigid flex

class Substitute r f a

Constraint simplification

type CTrans r f

simplify1

ifLe

compareOffset

Printing

Wellformedness

class ValidOffset a

class TruncateOffset a

Computing variable sets

class Rigids r a

class Flexs flex a