<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"><html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>Agda.TypeChecking.SizedTypes</title><link href="ocean.css" rel="stylesheet" type="text/css" title="Ocean" /><script src="haddock-util.js" type="text/javascript"></script><script type="text/javascript">//<![CDATA[
window.onload = function () {pageLoad();setSynopsis("mini_Agda-TypeChecking-SizedTypes.html");};
//]]>
</script></head><body><div id="package-header"><ul class="links" id="page-menu"><li><a href="src/Agda-TypeChecking-SizedTypes.html">Source</a></li><li><a href="index.html">Contents</a></li><li><a href="doc-index.html">Index</a></li></ul><p class="caption">Agda-2.3.2.1: A dependently typed functional programming language and proof assistant</p></div><div id="content"><div id="module-header"><table class="info"><tr><th>Safe Haskell</th><td>None</td></tr></table><p class="caption">Agda.TypeChecking.SizedTypes</p></div><div id="synopsis"><p id="control.syn" class="caption expander" onclick="toggleSection('syn')">Synopsis</p><ul id="section.syn" class="hide" onclick="toggleSection('syn')"><li class="src short"><a href="#v:builtinSizeHook">builtinSizeHook</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> -> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a></li><li class="src short"><a href="#v:deepSizeView">deepSizeView</a> :: <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-Monad-SizedTypes.html#t:DeepSizeView">DeepSizeView</a></li><li class="src short"><a href="#v:sizeMaxView">sizeMaxView</a> :: <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-Monad-SizedTypes.html#t:SizeMaxView">SizeMaxView</a></li><li class="src short"><a href="#v:trySizeUniv">trySizeUniv</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:Comparison">Comparison</a> -> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> [<a href="Agda-Syntax-Internal.html#t:Elim">Elim</a>] -> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> [<a href="Agda-Syntax-Internal.html#t:Elim">Elim</a>] -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a></li><li class="src short"><a href="#v:compareSizes">compareSizes</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:Comparison">Comparison</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a></li><li class="src short"><a href="#v:compareMaxViews">compareMaxViews</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:Comparison">Comparison</a> -> <a href="Agda-TypeChecking-Monad-SizedTypes.html#t:SizeMaxView">SizeMaxView</a> -> <a href="Agda-TypeChecking-Monad-SizedTypes.html#t:SizeMaxView">SizeMaxView</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a></li><li class="src short"><a href="#v:compareBelowMax">compareBelowMax</a> :: <a href="Agda-TypeChecking-Monad-SizedTypes.html#t:DeepSizeView">DeepSizeView</a> -> <a href="Agda-TypeChecking-Monad-SizedTypes.html#t:SizeMaxView">SizeMaxView</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a></li><li class="src short"><a href="#v:compareSizeViews">compareSizeViews</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:Comparison">Comparison</a> -> <a href="Agda-TypeChecking-Monad-SizedTypes.html#t:DeepSizeView">DeepSizeView</a> -> <a href="Agda-TypeChecking-Monad-SizedTypes.html#t:DeepSizeView">DeepSizeView</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a></li><li class="src short"><a href="#v:isBounded">isBounded</a> :: <a href="Agda-Syntax-Common.html#t:Nat">Nat</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-Monad-SizedTypes.html#t:BoundedSize">BoundedSize</a></li><li class="src short"><a href="#v:trivial">trivial</a> :: <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li class="src short"><a href="#v:boundedSizeMetaHook">boundedSizeMetaHook</a> :: <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-Syntax-Internal.html#t:Telescope">Telescope</a> -> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a></li><li class="src short"><a href="#v:isSizeProblem">isSizeProblem</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:ProblemId">ProblemId</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li class="src short"><a href="#v:isSizeConstraint">isSizeConstraint</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:Closure">Closure</a> <a href="Agda-TypeChecking-Monad-Base.html#t:Constraint">Constraint</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li class="src short"><a href="#v:getSizeConstraints">getSizeConstraints</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> [<a href="Agda-TypeChecking-Monad-Base.html#t:Closure">Closure</a> <a href="Agda-TypeChecking-Monad-Base.html#t:Constraint">Constraint</a>]</li><li class="src short"><a href="#v:getSizeMetas">getSizeMetas</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> [(<a href="Agda-Syntax-Internal.html#t:MetaId">MetaId</a>, <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a>)]</li><li class="src short"><span class="keyword">data</span> <a href="#t:SizeExpr">SizeExpr</a> <ul class="subs"><li>= <a href="#v:SizeMeta">SizeMeta</a> <a href="Agda-Syntax-Internal.html#t:MetaId">MetaId</a> [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a>] </li><li>| <a href="#v:Rigid">Rigid</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a> </li></ul></li><li class="src short"><span class="keyword">data</span> <a href="#t:SizeConstraint">SizeConstraint</a> = <a href="#v:Leq">Leq</a> <a href="Agda-TypeChecking-SizedTypes.html#t:SizeExpr">SizeExpr</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a> <a href="Agda-TypeChecking-SizedTypes.html#t:SizeExpr">SizeExpr</a></li><li class="src short"><a href="#v:computeSizeConstraints">computeSizeConstraints</a> :: [<a href="Agda-TypeChecking-Monad-Base.html#t:Closure">Closure</a> <a href="Agda-TypeChecking-Monad-Base.html#t:Constraint">Constraint</a>] -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> [<a href="Agda-TypeChecking-SizedTypes.html#t:SizeConstraint">SizeConstraint</a>]</li><li class="src short"><a href="#v:computeSizeConstraint">computeSizeConstraint</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:Constraint">Constraint</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> <a href="Agda-TypeChecking-SizedTypes.html#t:SizeConstraint">SizeConstraint</a>)</li><li class="src short"><a href="#v:sizeExpr">sizeExpr</a> :: <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> (<a href="Agda-TypeChecking-SizedTypes.html#t:SizeExpr">SizeExpr</a>, <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a>)</li><li class="src short"><a href="#v:flexibleVariables">flexibleVariables</a> :: <a href="Agda-TypeChecking-SizedTypes.html#t:SizeConstraint">SizeConstraint</a> -> [(<a href="Agda-Syntax-Internal.html#t:MetaId">MetaId</a>, [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a>])]</li><li class="src short"><a href="#v:haveSizedTypes">haveSizedTypes</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li class="src short"><a href="#v:canonicalizeSizeConstraint">canonicalizeSizeConstraint</a> :: <a href="Agda-TypeChecking-SizedTypes.html#t:SizeConstraint">SizeConstraint</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> <a href="Agda-TypeChecking-SizedTypes.html#t:SizeConstraint">SizeConstraint</a></li><li class="src short"><a href="#v:solveSizeConstraints">solveSizeConstraints</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a></li></ul></div><div id="interface"><h1>Documentation</h1><div class="top"><p class="src"><a name="v:builtinSizeHook" class="def">builtinSizeHook</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> -> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a><a href="src/Agda-TypeChecking-SizedTypes.html#builtinSizeHook" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:deepSizeView" class="def">deepSizeView</a> :: <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-Monad-SizedTypes.html#t:DeepSizeView">DeepSizeView</a><a href="src/Agda-TypeChecking-SizedTypes.html#deepSizeView" class="link">Source</a></p><div class="doc"><p>Compute the deep size view of a term.
Precondition: sized types are enabled.
</p></div></div><div class="top"><p class="src"><a name="v:sizeMaxView" class="def">sizeMaxView</a> :: <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-Monad-SizedTypes.html#t:SizeMaxView">SizeMaxView</a><a href="src/Agda-TypeChecking-SizedTypes.html#sizeMaxView" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:trySizeUniv" class="def">trySizeUniv</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:Comparison">Comparison</a> -> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> [<a href="Agda-Syntax-Internal.html#t:Elim">Elim</a>] -> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> [<a href="Agda-Syntax-Internal.html#t:Elim">Elim</a>] -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a><a href="src/Agda-TypeChecking-SizedTypes.html#trySizeUniv" class="link">Source</a></p><div class="doc"><p>Account for subtyping <code>Size< i =< Size</code>
Preconditions:
<code>m = x els1</code>, <code>n = y els2</code>, <code>m</code> and <code>n</code> are not equal.
</p></div></div><div class="top"><p class="src"><a name="v:compareSizes" class="def">compareSizes</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:Comparison">Comparison</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a><a href="src/Agda-TypeChecking-SizedTypes.html#compareSizes" class="link">Source</a></p><div class="doc"><p>Compare two sizes. Only with --sized-types.
</p></div></div><div class="top"><p class="src"><a name="v:compareMaxViews" class="def">compareMaxViews</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:Comparison">Comparison</a> -> <a href="Agda-TypeChecking-Monad-SizedTypes.html#t:SizeMaxView">SizeMaxView</a> -> <a href="Agda-TypeChecking-Monad-SizedTypes.html#t:SizeMaxView">SizeMaxView</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a><a href="src/Agda-TypeChecking-SizedTypes.html#compareMaxViews" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:compareBelowMax" class="def">compareBelowMax</a> :: <a href="Agda-TypeChecking-Monad-SizedTypes.html#t:DeepSizeView">DeepSizeView</a> -> <a href="Agda-TypeChecking-Monad-SizedTypes.html#t:SizeMaxView">SizeMaxView</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a><a href="src/Agda-TypeChecking-SizedTypes.html#compareBelowMax" class="link">Source</a></p><div class="doc"><p><code>compareBelowMax u vs</code> checks <code>u <a href="= max vs@. Precondition: @size vs ">= max vs@. Precondition: @size vs </a>= 2</code>
</p></div></div><div class="top"><p class="src"><a name="v:compareSizeViews" class="def">compareSizeViews</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:Comparison">Comparison</a> -> <a href="Agda-TypeChecking-Monad-SizedTypes.html#t:DeepSizeView">DeepSizeView</a> -> <a href="Agda-TypeChecking-Monad-SizedTypes.html#t:DeepSizeView">DeepSizeView</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a><a href="src/Agda-TypeChecking-SizedTypes.html#compareSizeViews" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:isBounded" class="def">isBounded</a> :: <a href="Agda-Syntax-Common.html#t:Nat">Nat</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-Monad-SizedTypes.html#t:BoundedSize">BoundedSize</a><a href="src/Agda-TypeChecking-SizedTypes.html#isBounded" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:trivial" class="def">trivial</a> :: <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a><a href="src/Agda-TypeChecking-SizedTypes.html#trivial" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:boundedSizeMetaHook" class="def">boundedSizeMetaHook</a> :: <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-Syntax-Internal.html#t:Telescope">Telescope</a> -> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a><a href="src/Agda-TypeChecking-SizedTypes.html#boundedSizeMetaHook" class="link">Source</a></p><div class="doc"><p>Whenever we create a bounded size meta, add a constraint
expressing the bound.
In <code>boundedSizeMetaHook v tel a</code>, <code>tel</code> includes the current context.
</p></div></div><div class="top"><p class="src"><a name="v:isSizeProblem" class="def">isSizeProblem</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:ProblemId">ProblemId</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a><a href="src/Agda-TypeChecking-SizedTypes.html#isSizeProblem" class="link">Source</a></p><div class="doc"><p>Test whether a problem consists only of size constraints.
</p></div></div><div class="top"><p class="src"><a name="v:isSizeConstraint" class="def">isSizeConstraint</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:Closure">Closure</a> <a href="Agda-TypeChecking-Monad-Base.html#t:Constraint">Constraint</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a><a href="src/Agda-TypeChecking-SizedTypes.html#isSizeConstraint" class="link">Source</a></p><div class="doc"><p>Test is a constraint speaks about sizes.
</p></div></div><div class="top"><p class="src"><a name="v:getSizeConstraints" class="def">getSizeConstraints</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> [<a href="Agda-TypeChecking-Monad-Base.html#t:Closure">Closure</a> <a href="Agda-TypeChecking-Monad-Base.html#t:Constraint">Constraint</a>]<a href="src/Agda-TypeChecking-SizedTypes.html#getSizeConstraints" class="link">Source</a></p><div class="doc"><p>Find the size constraints.
</p></div></div><div class="top"><p class="src"><a name="v:getSizeMetas" class="def">getSizeMetas</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> [(<a href="Agda-Syntax-Internal.html#t:MetaId">MetaId</a>, <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a>)]<a href="src/Agda-TypeChecking-SizedTypes.html#getSizeMetas" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:SizeExpr" class="def">SizeExpr</a> <a href="src/Agda-TypeChecking-SizedTypes.html#SizeExpr" class="link">Source</a></p><div class="doc"><p>Atomic size expressions.
</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:SizeMeta" class="def">SizeMeta</a> <a href="Agda-Syntax-Internal.html#t:MetaId">MetaId</a> [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a>]</td><td class="doc"><p>A size meta applied to de Bruijn levels.
</p></td></tr><tr><td class="src"><a name="v:Rigid" class="def">Rigid</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a></td><td class="doc"><p>A de Bruijn level.
</p></td></tr></table></div><div class="subs instances"><p id="control.i:SizeExpr" class="caption collapser" onclick="toggleSection('i:SizeExpr')">Instances</p><div id="section.i:SizeExpr" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Eq.html#t:Eq">Eq</a> <a href="Agda-TypeChecking-SizedTypes.html#t:SizeExpr">SizeExpr</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Text-Show.html#t:Show">Show</a> <a href="Agda-TypeChecking-SizedTypes.html#t:SizeExpr">SizeExpr</a></td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:SizeConstraint" class="def">SizeConstraint</a> <a href="src/Agda-TypeChecking-SizedTypes.html#SizeConstraint" class="link">Source</a></p><div class="doc"><p>Size constraints we can solve.
</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:Leq" class="def">Leq</a> <a href="Agda-TypeChecking-SizedTypes.html#t:SizeExpr">SizeExpr</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a> <a href="Agda-TypeChecking-SizedTypes.html#t:SizeExpr">SizeExpr</a></td><td class="doc"><p><code>Leq a +n b</code> represents <code>a =< b + n</code>.
<code>Leq a -n b</code> represents <code>a + n =< b</code>.
</p></td></tr></table></div><div class="subs instances"><p id="control.i:SizeConstraint" class="caption collapser" onclick="toggleSection('i:SizeConstraint')">Instances</p><div id="section.i:SizeConstraint" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Text-Show.html#t:Show">Show</a> <a href="Agda-TypeChecking-SizedTypes.html#t:SizeConstraint">SizeConstraint</a></td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><a name="v:computeSizeConstraints" class="def">computeSizeConstraints</a> :: [<a href="Agda-TypeChecking-Monad-Base.html#t:Closure">Closure</a> <a href="Agda-TypeChecking-Monad-Base.html#t:Constraint">Constraint</a>] -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> [<a href="Agda-TypeChecking-SizedTypes.html#t:SizeConstraint">SizeConstraint</a>]<a href="src/Agda-TypeChecking-SizedTypes.html#computeSizeConstraints" class="link">Source</a></p><div class="doc"><p>Compute a set of size constraints that all live in the same context
from constraints over terms of type size that may live in different
contexts.
</p><p>cf. <code><a href="Agda-TypeChecking-LevelConstraints.html#v:simplifyLevelConstraint">simplifyLevelConstraint</a></code>
</p></div></div><div class="top"><p class="src"><a name="v:computeSizeConstraint" class="def">computeSizeConstraint</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:Constraint">Constraint</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> <a href="Agda-TypeChecking-SizedTypes.html#t:SizeConstraint">SizeConstraint</a>)<a href="src/Agda-TypeChecking-SizedTypes.html#computeSizeConstraint" class="link">Source</a></p><div class="doc"><p>Turn a constraint over de Bruijn levels into a size constraint.
</p></div></div><div class="top"><p class="src"><a name="v:sizeExpr" class="def">sizeExpr</a> :: <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> (<a href="Agda-TypeChecking-SizedTypes.html#t:SizeExpr">SizeExpr</a>, <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a>)<a href="src/Agda-TypeChecking-SizedTypes.html#sizeExpr" class="link">Source</a></p><div class="doc"><p>Turn a term with de Bruijn levels into a size expression with offset.
</p><p>Throws a <code><a href="Agda-TypeChecking-Monad-Base.html#v:patternViolation">patternViolation</a></code> if the term isn't a proper size expression.
</p></div></div><div class="top"><p class="src"><a name="v:flexibleVariables" class="def">flexibleVariables</a> :: <a href="Agda-TypeChecking-SizedTypes.html#t:SizeConstraint">SizeConstraint</a> -> [(<a href="Agda-Syntax-Internal.html#t:MetaId">MetaId</a>, [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a>])]<a href="src/Agda-TypeChecking-SizedTypes.html#flexibleVariables" class="link">Source</a></p><div class="doc"><p>Compute list of size metavariables with their arguments
appearing in a constraint.
</p></div></div><div class="top"><p class="src"><a name="v:haveSizedTypes" class="def">haveSizedTypes</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a><a href="src/Agda-TypeChecking-SizedTypes.html#haveSizedTypes" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:canonicalizeSizeConstraint" class="def">canonicalizeSizeConstraint</a> :: <a href="Agda-TypeChecking-SizedTypes.html#t:SizeConstraint">SizeConstraint</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> <a href="Agda-TypeChecking-SizedTypes.html#t:SizeConstraint">SizeConstraint</a><a href="src/Agda-TypeChecking-SizedTypes.html#canonicalizeSizeConstraint" class="link">Source</a></p><div class="doc"><p>Convert size constraint into form where each meta is applied
to levels <code>0,1,..,n-1</code> where <code>n</code> is the arity of that meta.
</p><p><code>X[σ] <= t</code> beomes <code>X[id] <= t[σ^-1]</code>
</p><p><code>X[σ] ≤ Y[τ]</code> becomes <code>X[id] ≤ Y[τ[σ^-1]]</code> or <code>X[σ[τ^1]] ≤ Y[id]</code>
whichever is defined. If none is defined, we give up.
</p></div></div><div class="top"><p class="src"><a name="v:solveSizeConstraints" class="def">solveSizeConstraints</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a><a href="src/Agda-TypeChecking-SizedTypes.html#solveSizeConstraints" class="link">Source</a></p></div></div></div><div id="footer"><p>Produced by <a href="http://www.haskell.org/haddock/">Haddock</a> version 2.11.0</p></div></body></html>
