<!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.Substitute</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-Substitute.html");};
//]]>
</script></head><body><div id="package-header"><ul class="links" id="page-menu"><li><a href="src/Agda-TypeChecking-Substitute.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.Substitute</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"><span class="keyword">class</span> <a href="#t:Apply">Apply</a> t <span class="keyword">where</span><ul class="subs"><li><a href="#v:apply">apply</a> :: t -> <a href="Agda-Syntax-Internal.html#t:Args">Args</a> -> t</li></ul></li><li class="src short"><a href="#v:piApply">piApply</a> :: <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-Syntax-Internal.html#t:Args">Args</a> -> <a href="Agda-Syntax-Internal.html#t:Type">Type</a></li><li class="src short"><span class="keyword">class</span> <a href="#t:Abstract">Abstract</a> t <span class="keyword">where</span><ul class="subs"><li><a href="#v:abstract">abstract</a> :: <a href="Agda-Syntax-Internal.html#t:Telescope">Telescope</a> -> t -> t</li></ul></li><li class="src short"><a href="#v:telVars">telVars</a> :: <a href="Agda-Syntax-Internal.html#t:Telescope">Telescope</a> -> [<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> <a href="Agda-Syntax-Internal.html#t:Pattern">Pattern</a>]</li><li class="src short"><a href="#v:abstractArgs">abstractArgs</a> :: <a href="Agda-TypeChecking-Substitute.html#t:Abstract">Abstract</a> a => <a href="Agda-Syntax-Internal.html#t:Args">Args</a> -> a -> a</li><li class="src short"><span class="keyword">data</span> <a href="#t:Substitution">Substitution</a> <ul class="subs"><li>= <a href="#v:IdS">IdS</a> </li><li>| <a href="#v:EmptyS">EmptyS</a> </li><li>| <a href="#v:Wk">Wk</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-Substitute.html#t:Substitution">Substitution</a> </li><li>| <a href="Agda-Syntax-Internal.html#t:Term">Term</a> <a href="#v::-35-">:#</a> <a href="Agda-TypeChecking-Substitute.html#t:Substitution">Substitution</a> </li><li>| <a href="#v:Lift">Lift</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-Substitute.html#t:Substitution">Substitution</a> </li></ul></li><li class="src short"><a href="#v:idS">idS</a> :: <a href="Agda-TypeChecking-Substitute.html#t:Substitution">Substitution</a></li><li class="src short"><a href="#v:wkS">wkS</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-Substitute.html#t:Substitution">Substitution</a> -> <a href="Agda-TypeChecking-Substitute.html#t:Substitution">Substitution</a></li><li class="src short"><a href="#v:raiseS">raiseS</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-Substitute.html#t:Substitution">Substitution</a></li><li class="src short"><a href="#v:singletonS">singletonS</a> :: <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Substitute.html#t:Substitution">Substitution</a></li><li class="src short"><a href="#v:liftS">liftS</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-Substitute.html#t:Substitution">Substitution</a> -> <a href="Agda-TypeChecking-Substitute.html#t:Substitution">Substitution</a></li><li class="src short"><a href="#v:dropS">dropS</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-Substitute.html#t:Substitution">Substitution</a> -> <a href="Agda-TypeChecking-Substitute.html#t:Substitution">Substitution</a></li><li class="src short"><a href="#v:composeS">composeS</a> :: <a href="Agda-TypeChecking-Substitute.html#t:Substitution">Substitution</a> -> <a href="Agda-TypeChecking-Substitute.html#t:Substitution">Substitution</a> -> <a href="Agda-TypeChecking-Substitute.html#t:Substitution">Substitution</a></li><li class="src short"><a href="#v:splitS">splitS</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-Substitute.html#t:Substitution">Substitution</a> -> (<a href="Agda-TypeChecking-Substitute.html#t:Substitution">Substitution</a>, <a href="Agda-TypeChecking-Substitute.html#t:Substitution">Substitution</a>)</li><li class="src short"><a href="#v:-43--43--35-">(++#)</a> :: [<a href="Agda-Syntax-Internal.html#t:Term">Term</a>] -> <a href="Agda-TypeChecking-Substitute.html#t:Substitution">Substitution</a> -> <a href="Agda-TypeChecking-Substitute.html#t:Substitution">Substitution</a></li><li class="src short"><a href="#v:parallelS">parallelS</a> :: [<a href="Agda-Syntax-Internal.html#t:Term">Term</a>] -> <a href="Agda-TypeChecking-Substitute.html#t:Substitution">Substitution</a></li><li class="src short"><a href="#v:lookupS">lookupS</a> :: <a href="Agda-TypeChecking-Substitute.html#t:Substitution">Substitution</a> -> <a href="Agda-Syntax-Common.html#t:Nat">Nat</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a></li><li class="src short"><span class="keyword">class</span> <a href="#t:Subst">Subst</a> t <span class="keyword">where</span><ul class="subs"><li><a href="#v:applySubst">applySubst</a> :: <a href="Agda-TypeChecking-Substitute.html#t:Substitution">Substitution</a> -> t -> t</li></ul></li><li class="src short"><a href="#v:raise">raise</a> :: <a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> t => <a href="Agda-Syntax-Common.html#t:Nat">Nat</a> -> t -> t</li><li class="src short"><a href="#v:raiseFrom">raiseFrom</a> :: <a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> t => <a href="Agda-Syntax-Common.html#t:Nat">Nat</a> -> <a href="Agda-Syntax-Common.html#t:Nat">Nat</a> -> t -> t</li><li class="src short"><a href="#v:subst">subst</a> :: <a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> t => <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> t -> t</li><li class="src short"><a href="#v:substUnder">substUnder</a> :: <a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> t => <a href="Agda-Syntax-Common.html#t:Nat">Nat</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> t -> t</li><li class="src short"><span class="keyword">data</span> <a href="#t:TelV">TelV</a> a = <a href="#v:TelV">TelV</a> (<a href="Agda-Syntax-Internal.html#t:Tele">Tele</a> (<a href="Agda-Syntax-Common.html#t:Dom">Dom</a> a)) a</li><li class="src short"><span class="keyword">type</span> <a href="#t:TelView">TelView</a> = <a href="Agda-TypeChecking-Substitute.html#t:TelV">TelV</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a></li><li class="src short"><a href="#v:telFromList">telFromList</a> :: [<a href="Agda-Syntax-Common.html#t:Dom">Dom</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-Internal.html#t:Type">Type</a>)] -> <a href="Agda-Syntax-Internal.html#t:Telescope">Telescope</a></li><li class="src short"><a href="#v:telToList">telToList</a> :: <a href="Agda-Syntax-Internal.html#t:Telescope">Telescope</a> -> [<a href="Agda-Syntax-Common.html#t:Dom">Dom</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-Internal.html#t:Type">Type</a>)]</li><li class="src short"><a href="#v:telView-39-">telView'</a> :: <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-TypeChecking-Substitute.html#t:TelView">TelView</a></li><li class="src short"><a href="#v:mkPi">mkPi</a> :: <a href="Agda-Syntax-Common.html#t:Dom">Dom</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-Internal.html#t:Type">Type</a>) -> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-Syntax-Internal.html#t:Type">Type</a></li><li class="src short"><a href="#v:telePi">telePi</a> :: <a href="Agda-Syntax-Internal.html#t:Telescope">Telescope</a> -> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-Syntax-Internal.html#t:Type">Type</a></li><li class="src short"><a href="#v:telePi_">telePi_</a> :: <a href="Agda-Syntax-Internal.html#t:Telescope">Telescope</a> -> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-Syntax-Internal.html#t:Type">Type</a></li><li class="src short"><a href="#v:teleLam">teleLam</a> :: <a href="Agda-Syntax-Internal.html#t:Telescope">Telescope</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a></li><li class="src short"><a href="#v:dLub">dLub</a> :: <a href="Agda-Syntax-Internal.html#t:Sort">Sort</a> -> <a href="Agda-Syntax-Internal.html#t:Abs">Abs</a> <a href="Agda-Syntax-Internal.html#t:Sort">Sort</a> -> <a href="Agda-Syntax-Internal.html#t:Sort">Sort</a></li><li class="src short"><a href="#v:absApp">absApp</a> :: <a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> t => <a href="Agda-Syntax-Internal.html#t:Abs">Abs</a> t -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> t</li><li class="src short"><a href="#v:absBody">absBody</a> :: <a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> t => <a href="Agda-Syntax-Internal.html#t:Abs">Abs</a> t -> t</li><li class="src short"><a href="#v:mkAbs">mkAbs</a> :: (<a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> a, <a href="Agda-TypeChecking-Free.html#t:Free">Free</a> a) => <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> -> a -> <a href="Agda-Syntax-Internal.html#t:Abs">Abs</a> a</li><li class="src short"><a href="#v:reAbs">reAbs</a> :: (<a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> a, <a href="Agda-TypeChecking-Free.html#t:Free">Free</a> a) => <a href="Agda-Syntax-Internal.html#t:Abs">Abs</a> a -> <a href="Agda-Syntax-Internal.html#t:Abs">Abs</a> a</li><li class="src short"><a href="#v:underAbs">underAbs</a> :: <a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> a => (a -> b -> b) -> a -> <a href="Agda-Syntax-Internal.html#t:Abs">Abs</a> b -> <a href="Agda-Syntax-Internal.html#t:Abs">Abs</a> b</li><li class="src short"><a href="#v:underLambdas">underLambdas</a> :: <a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> a => <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a> -> (a -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a>) -> a -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a></li><li class="src short"><a href="#v:sLub">sLub</a> :: <a href="Agda-Syntax-Internal.html#t:Sort">Sort</a> -> <a href="Agda-Syntax-Internal.html#t:Sort">Sort</a> -> <a href="Agda-Syntax-Internal.html#t:Sort">Sort</a></li><li class="src short"><a href="#v:lvlView">lvlView</a> :: <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-Syntax-Internal.html#t:Level">Level</a></li><li class="src short"><a href="#v:levelMax">levelMax</a> :: [<a href="Agda-Syntax-Internal.html#t:PlusLevel">PlusLevel</a>] -> <a href="Agda-Syntax-Internal.html#t:Level">Level</a></li><li class="src short"><a href="#v:sortTm">sortTm</a> :: <a href="Agda-Syntax-Internal.html#t:Sort">Sort</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a></li><li class="src short"><a href="#v:levelSort">levelSort</a> :: <a href="Agda-Syntax-Internal.html#t:Level">Level</a> -> <a href="Agda-Syntax-Internal.html#t:Sort">Sort</a></li><li class="src short"><a href="#v:levelTm">levelTm</a> :: <a href="Agda-Syntax-Internal.html#t:Level">Level</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a></li><li class="src short"><a href="#v:unLevelAtom">unLevelAtom</a> :: <a href="Agda-Syntax-Internal.html#t:LevelAtom">LevelAtom</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a></li></ul></div><div id="interface"><h1>Documentation</h1><div class="top"><p class="src"><span class="keyword">class</span> <a name="t:Apply" class="def">Apply</a> t <span class="keyword">where</span><a href="src/Agda-TypeChecking-Substitute.html#Apply" class="link">Source</a></p><div class="doc"><p>Apply something to a bunch of arguments.
Preserves blocking tags (application can never resolve blocking).
</p></div><div class="subs methods"><p class="caption">Methods</p><p class="src"><a name="v:apply" class="def">apply</a> :: t -> <a href="Agda-Syntax-Internal.html#t:Args">Args</a> -> t<a href="src/Agda-TypeChecking-Substitute.html#apply" class="link">Source</a></p></div><div class="subs instances"><p id="control.i:Apply" class="caption collapser" onclick="toggleSection('i:Apply')">Instances</p><div id="section.i:Apply" class="show"><table><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Apply">Apply</a> <a href="Agda-Utils-Permutation.html#t:Permutation">Permutation</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Apply">Apply</a> <a href="Agda-Syntax-Internal.html#t:ClauseBody">ClauseBody</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Apply">Apply</a> <a href="Agda-Syntax-Internal.html#t:Clause">Clause</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Apply">Apply</a> <a href="Agda-Syntax-Internal.html#t:Sort">Sort</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Apply">Apply</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Apply">Apply</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Apply">Apply</a> <a href="Agda-TypeChecking-CompiledClause.html#t:CompiledClauses">CompiledClauses</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Apply">Apply</a> <a href="Agda-TypeChecking-Monad-Base.html#t:FunctionInverse">FunctionInverse</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Apply">Apply</a> <a href="Agda-TypeChecking-Monad-Base.html#t:PrimFun">PrimFun</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Apply">Apply</a> <a href="Agda-TypeChecking-Monad-Base.html#t:Defn">Defn</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Apply">Apply</a> <a href="Agda-TypeChecking-Monad-Base.html#t:Definition">Definition</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Apply">Apply</a> <a href="Agda-TypeChecking-Monad-Base.html#t:DisplayTerm">DisplayTerm</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Apply">Apply</a> t => <a href="Agda-TypeChecking-Substitute.html#t:Apply">Apply</a> [t]</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Apply">Apply</a> [<a href="Agda-TypeChecking-Monad-Base.html#t:Occurrence">Occurrence</a>]</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Apply">Apply</a> [<a href="Agda-TypeChecking-Monad-Base.html#t:Polarity">Polarity</a>]</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Apply">Apply</a> t => <a href="Agda-TypeChecking-Substitute.html#t:Apply">Apply</a> (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> t)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Apply">Apply</a> a => <a href="Agda-TypeChecking-Substitute.html#t:Apply">Apply</a> (<a href="Agda-Utils-Pointer.html#t:Ptr">Ptr</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Apply">Apply</a> t => <a href="Agda-TypeChecking-Substitute.html#t:Apply">Apply</a> (<a href="Agda-Syntax-Internal.html#t:Blocked">Blocked</a> t)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> a => <a href="Agda-TypeChecking-Substitute.html#t:Apply">Apply</a> (<a href="Agda-Syntax-Internal.html#t:Tele">Tele</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Apply">Apply</a> a => <a href="Agda-TypeChecking-Substitute.html#t:Apply">Apply</a> (<a href="Agda-TypeChecking-CompiledClause.html#t:Case">Case</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Apply">Apply</a> a => <a href="Agda-TypeChecking-Substitute.html#t:Apply">Apply</a> (<a href="Agda-TypeChecking-CompiledClause.html#t:WithArity">WithArity</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src">(<a href="Agda-TypeChecking-Substitute.html#t:Apply">Apply</a> a, <a href="Agda-TypeChecking-Substitute.html#t:Apply">Apply</a> b) => <a href="Agda-TypeChecking-Substitute.html#t:Apply">Apply</a> (a, b)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Apply">Apply</a> v => <a href="Agda-TypeChecking-Substitute.html#t:Apply">Apply</a> (<a href="/usr/share/doc/ghc/html/libraries/containers-0.4.2.1/Data-Map.html#t:Map">Map</a> k v)</td><td class="doc empty"> </td></tr><tr><td class="src">(<a href="Agda-TypeChecking-Substitute.html#t:Apply">Apply</a> a, <a href="Agda-TypeChecking-Substitute.html#t:Apply">Apply</a> b, <a href="Agda-TypeChecking-Substitute.html#t:Apply">Apply</a> c) => <a href="Agda-TypeChecking-Substitute.html#t:Apply">Apply</a> (a, b, c)</td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><a name="v:piApply" class="def">piApply</a> :: <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-Syntax-Internal.html#t:Args">Args</a> -> <a href="Agda-Syntax-Internal.html#t:Type">Type</a><a href="src/Agda-TypeChecking-Substitute.html#piApply" class="link">Source</a></p><div class="doc"><p>The type must contain the right number of pis without have to perform any
reduction.
</p></div></div><div class="top"><p class="src"><span class="keyword">class</span> <a name="t:Abstract" class="def">Abstract</a> t <span class="keyword">where</span><a href="src/Agda-TypeChecking-Substitute.html#Abstract" class="link">Source</a></p><div class="doc"><p><code>(abstract args v) args --> v[args]</code>.
</p></div><div class="subs methods"><p class="caption">Methods</p><p class="src"><a name="v:abstract" class="def">abstract</a> :: <a href="Agda-Syntax-Internal.html#t:Telescope">Telescope</a> -> t -> t<a href="src/Agda-TypeChecking-Substitute.html#abstract" class="link">Source</a></p></div><div class="subs instances"><p id="control.i:Abstract" class="caption collapser" onclick="toggleSection('i:Abstract')">Instances</p><div id="section.i:Abstract" class="show"><table><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Abstract">Abstract</a> <a href="Agda-Utils-Permutation.html#t:Permutation">Permutation</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Abstract">Abstract</a> <a href="Agda-Syntax-Internal.html#t:ClauseBody">ClauseBody</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Abstract">Abstract</a> <a href="Agda-Syntax-Internal.html#t:Clause">Clause</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Abstract">Abstract</a> <a href="Agda-Syntax-Internal.html#t:Sort">Sort</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Abstract">Abstract</a> <a href="Agda-Syntax-Internal.html#t:Telescope">Telescope</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Abstract">Abstract</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Abstract">Abstract</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Abstract">Abstract</a> <a href="Agda-TypeChecking-CompiledClause.html#t:CompiledClauses">CompiledClauses</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Abstract">Abstract</a> <a href="Agda-TypeChecking-Monad-Base.html#t:FunctionInverse">FunctionInverse</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Abstract">Abstract</a> <a href="Agda-TypeChecking-Monad-Base.html#t:PrimFun">PrimFun</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Abstract">Abstract</a> <a href="Agda-TypeChecking-Monad-Base.html#t:Defn">Defn</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Abstract">Abstract</a> <a href="Agda-TypeChecking-Monad-Base.html#t:Definition">Definition</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Abstract">Abstract</a> t => <a href="Agda-TypeChecking-Substitute.html#t:Abstract">Abstract</a> [t]</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Abstract">Abstract</a> [<a href="Agda-TypeChecking-Monad-Base.html#t:Occurrence">Occurrence</a>]</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Abstract">Abstract</a> [<a href="Agda-TypeChecking-Monad-Base.html#t:Polarity">Polarity</a>]</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Abstract">Abstract</a> t => <a href="Agda-TypeChecking-Substitute.html#t:Abstract">Abstract</a> (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> t)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Abstract">Abstract</a> a => <a href="Agda-TypeChecking-Substitute.html#t:Abstract">Abstract</a> (<a href="Agda-TypeChecking-CompiledClause.html#t:Case">Case</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Abstract">Abstract</a> a => <a href="Agda-TypeChecking-Substitute.html#t:Abstract">Abstract</a> (<a href="Agda-TypeChecking-CompiledClause.html#t:WithArity">WithArity</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Abstract">Abstract</a> v => <a href="Agda-TypeChecking-Substitute.html#t:Abstract">Abstract</a> (<a href="/usr/share/doc/ghc/html/libraries/containers-0.4.2.1/Data-Map.html#t:Map">Map</a> k v)</td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><a name="v:telVars" class="def">telVars</a> :: <a href="Agda-Syntax-Internal.html#t:Telescope">Telescope</a> -> [<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> <a href="Agda-Syntax-Internal.html#t:Pattern">Pattern</a>]<a href="src/Agda-TypeChecking-Substitute.html#telVars" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:abstractArgs" class="def">abstractArgs</a> :: <a href="Agda-TypeChecking-Substitute.html#t:Abstract">Abstract</a> a => <a href="Agda-Syntax-Internal.html#t:Args">Args</a> -> a -> a<a href="src/Agda-TypeChecking-Substitute.html#abstractArgs" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:Substitution" class="def">Substitution</a> <a href="src/Agda-TypeChecking-Substitute.html#Substitution" class="link">Source</a></p><div class="doc"><p>Substitutions.
</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:IdS" class="def">IdS</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:EmptyS" class="def">EmptyS</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:Wk" class="def">Wk</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-Substitute.html#t:Substitution">Substitution</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Internal.html#t:Term">Term</a> <a name="v::-35-" class="def">:#</a> <a href="Agda-TypeChecking-Substitute.html#t:Substitution">Substitution</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:Lift" class="def">Lift</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-Substitute.html#t:Substitution">Substitution</a></td><td class="doc empty"> </td></tr></table></div><div class="subs instances"><p id="control.i:Substitution" class="caption collapser" onclick="toggleSection('i:Substitution')">Instances</p><div id="section.i:Substitution" 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-Substitute.html#t:Substitution">Substitution</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/Data-Ord.html#t:Ord">Ord</a> <a href="Agda-TypeChecking-Substitute.html#t:Substitution">Substitution</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-Substitute.html#t:Substitution">Substitution</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Utils-Size.html#t:Sized">Sized</a> <a href="Agda-TypeChecking-Substitute.html#t:Substitution">Substitution</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Position.html#t:KillRange">KillRange</a> <a href="Agda-TypeChecking-Substitute.html#t:Substitution">Substitution</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> <a href="Agda-TypeChecking-Substitute.html#t:Substitution">Substitution</a></td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><a name="v:idS" class="def">idS</a> :: <a href="Agda-TypeChecking-Substitute.html#t:Substitution">Substitution</a><a href="src/Agda-TypeChecking-Substitute.html#idS" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:wkS" class="def">wkS</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-Substitute.html#t:Substitution">Substitution</a> -> <a href="Agda-TypeChecking-Substitute.html#t:Substitution">Substitution</a><a href="src/Agda-TypeChecking-Substitute.html#wkS" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:raiseS" class="def">raiseS</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-Substitute.html#t:Substitution">Substitution</a><a href="src/Agda-TypeChecking-Substitute.html#raiseS" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:singletonS" class="def">singletonS</a> :: <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Substitute.html#t:Substitution">Substitution</a><a href="src/Agda-TypeChecking-Substitute.html#singletonS" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:liftS" class="def">liftS</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-Substitute.html#t:Substitution">Substitution</a> -> <a href="Agda-TypeChecking-Substitute.html#t:Substitution">Substitution</a><a href="src/Agda-TypeChecking-Substitute.html#liftS" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:dropS" class="def">dropS</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-Substitute.html#t:Substitution">Substitution</a> -> <a href="Agda-TypeChecking-Substitute.html#t:Substitution">Substitution</a><a href="src/Agda-TypeChecking-Substitute.html#dropS" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:composeS" class="def">composeS</a> :: <a href="Agda-TypeChecking-Substitute.html#t:Substitution">Substitution</a> -> <a href="Agda-TypeChecking-Substitute.html#t:Substitution">Substitution</a> -> <a href="Agda-TypeChecking-Substitute.html#t:Substitution">Substitution</a><a href="src/Agda-TypeChecking-Substitute.html#composeS" class="link">Source</a></p><div class="doc"><pre>applySubst (ρ <code><a href="Agda-TypeChecking-Substitute.html#v:composeS">composeS</a></code> σ) v == applySubst ρ (applySubst σ v)</pre></div></div><div class="top"><p class="src"><a name="v:splitS" class="def">splitS</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-Substitute.html#t:Substitution">Substitution</a> -> (<a href="Agda-TypeChecking-Substitute.html#t:Substitution">Substitution</a>, <a href="Agda-TypeChecking-Substitute.html#t:Substitution">Substitution</a>)<a href="src/Agda-TypeChecking-Substitute.html#splitS" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:-43--43--35-" class="def">(++#)</a> :: [<a href="Agda-Syntax-Internal.html#t:Term">Term</a>] -> <a href="Agda-TypeChecking-Substitute.html#t:Substitution">Substitution</a> -> <a href="Agda-TypeChecking-Substitute.html#t:Substitution">Substitution</a><a href="src/Agda-TypeChecking-Substitute.html#%2B%2B%23" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:parallelS" class="def">parallelS</a> :: [<a href="Agda-Syntax-Internal.html#t:Term">Term</a>] -> <a href="Agda-TypeChecking-Substitute.html#t:Substitution">Substitution</a><a href="src/Agda-TypeChecking-Substitute.html#parallelS" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:lookupS" class="def">lookupS</a> :: <a href="Agda-TypeChecking-Substitute.html#t:Substitution">Substitution</a> -> <a href="Agda-Syntax-Common.html#t:Nat">Nat</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a><a href="src/Agda-TypeChecking-Substitute.html#lookupS" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">class</span> <a name="t:Subst" class="def">Subst</a> t <span class="keyword">where</span><a href="src/Agda-TypeChecking-Substitute.html#Subst" class="link">Source</a></p><div class="doc"><p>Apply a substitution.
</p></div><div class="subs methods"><p class="caption">Methods</p><p class="src"><a name="v:applySubst" class="def">applySubst</a> :: <a href="Agda-TypeChecking-Substitute.html#t:Substitution">Substitution</a> -> t -> t<a href="src/Agda-TypeChecking-Substitute.html#applySubst" class="link">Source</a></p></div><div class="subs instances"><p id="control.i:Subst" class="caption collapser" onclick="toggleSection('i:Subst')">Instances</p><div id="section.i:Subst" class="show"><table><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> ()</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> <a href="Agda-Syntax-Internal.html#t:Pattern">Pattern</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> <a href="Agda-Syntax-Internal.html#t:ClauseBody">ClauseBody</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> <a href="Agda-Syntax-Internal.html#t:LevelAtom">LevelAtom</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> <a href="Agda-Syntax-Internal.html#t:PlusLevel">PlusLevel</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> <a href="Agda-Syntax-Internal.html#t:Level">Level</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> <a href="Agda-Syntax-Internal.html#t:Sort">Sort</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> <a href="Agda-Syntax-Internal.html#t:Elim">Elim</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> <a href="Agda-TypeChecking-Monad-Base.html#t:DisplayTerm">DisplayTerm</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> <a href="Agda-TypeChecking-Monad-Base.html#t:DisplayForm">DisplayForm</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> <a href="Agda-TypeChecking-Monad-Base.html#t:Constraint">Constraint</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> <a href="Agda-TypeChecking-Substitute.html#t:Substitution">Substitution</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> <a href="Agda-TypeChecking-Rules-LHS-Problem.html#t:AsBinding">AsBinding</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> <a href="Agda-TypeChecking-Rules-LHS-Problem.html#t:DotPatternInst">DotPatternInst</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> <a href="Agda-TypeChecking-Rules-LHS-Problem.html#t:ProblemRest">ProblemRest</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Equality">Equality</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> a => <a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> [a]</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> a => <a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> a => <a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> (<a href="Agda-Utils-Pointer.html#t:Ptr">Ptr</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> a => <a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> a => <a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> (<a href="Agda-Syntax-Common.html#t:Dom">Dom</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> t => <a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> (<a href="Agda-Syntax-Internal.html#t:Blocked">Blocked</a> t)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> a => <a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> (<a href="Agda-Syntax-Internal.html#t:Tele">Tele</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> a => <a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> (<a href="Agda-Syntax-Internal.html#t:Abs">Abs</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> (<a href="Agda-TypeChecking-Rules-LHS-Problem.html#t:Problem-39-">Problem'</a> p)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> a => <a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> (<a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:HomHet">HomHet</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src">(<a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> a, <a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> b) => <a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> (a, b)</td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><a name="v:raise" class="def">raise</a> :: <a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> t => <a href="Agda-Syntax-Common.html#t:Nat">Nat</a> -> t -> t<a href="src/Agda-TypeChecking-Substitute.html#raise" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:raiseFrom" class="def">raiseFrom</a> :: <a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> t => <a href="Agda-Syntax-Common.html#t:Nat">Nat</a> -> <a href="Agda-Syntax-Common.html#t:Nat">Nat</a> -> t -> t<a href="src/Agda-TypeChecking-Substitute.html#raiseFrom" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:subst" class="def">subst</a> :: <a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> t => <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> t -> t<a href="src/Agda-TypeChecking-Substitute.html#subst" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:substUnder" class="def">substUnder</a> :: <a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> t => <a href="Agda-Syntax-Common.html#t:Nat">Nat</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> t -> t<a href="src/Agda-TypeChecking-Substitute.html#substUnder" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:TelV" class="def">TelV</a> a <a href="src/Agda-TypeChecking-Substitute.html#TelV" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:TelV" class="def">TelV</a> (<a href="Agda-Syntax-Internal.html#t:Tele">Tele</a> (<a href="Agda-Syntax-Common.html#t:Dom">Dom</a> a)) a</td><td class="doc empty"> </td></tr></table></div><div class="subs instances"><p id="control.i:TelV" class="caption collapser" onclick="toggleSection('i:TelV')">Instances</p><div id="section.i:TelV" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Control-Monad.html#t:Functor">Functor</a> <a href="Agda-TypeChecking-Substitute.html#t:TelV">TelV</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/Data-Typeable-Internal.html#t:Typeable1">Typeable1</a> <a href="Agda-TypeChecking-Substitute.html#t:TelV">TelV</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/Data-Eq.html#t:Eq">Eq</a> a, <a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> a) => <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Eq.html#t:Eq">Eq</a> (<a href="Agda-TypeChecking-Substitute.html#t:TelV">TelV</a> 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/Data-Ord.html#t:Ord">Ord</a> a, <a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> a) => <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Ord.html#t:Ord">Ord</a> (<a href="Agda-TypeChecking-Substitute.html#t:TelV">TelV</a> 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 => <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Text-Show.html#t:Show">Show</a> (<a href="Agda-TypeChecking-Substitute.html#t:TelV">TelV</a> a)</td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:TelView" class="def">TelView</a> = <a href="Agda-TypeChecking-Substitute.html#t:TelV">TelV</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a><a href="src/Agda-TypeChecking-Substitute.html#TelView" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:telFromList" class="def">telFromList</a> :: [<a href="Agda-Syntax-Common.html#t:Dom">Dom</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-Internal.html#t:Type">Type</a>)] -> <a href="Agda-Syntax-Internal.html#t:Telescope">Telescope</a><a href="src/Agda-TypeChecking-Substitute.html#telFromList" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:telToList" class="def">telToList</a> :: <a href="Agda-Syntax-Internal.html#t:Telescope">Telescope</a> -> [<a href="Agda-Syntax-Common.html#t:Dom">Dom</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-Internal.html#t:Type">Type</a>)]<a href="src/Agda-TypeChecking-Substitute.html#telToList" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:telView-39-" class="def">telView'</a> :: <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-TypeChecking-Substitute.html#t:TelView">TelView</a><a href="src/Agda-TypeChecking-Substitute.html#telView%27" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:mkPi" class="def">mkPi</a> :: <a href="Agda-Syntax-Common.html#t:Dom">Dom</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-Internal.html#t:Type">Type</a>) -> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-Syntax-Internal.html#t:Type">Type</a><a href="src/Agda-TypeChecking-Substitute.html#mkPi" class="link">Source</a></p><div class="doc"><pre>mkPi dom t = telePi (telFromList [dom]) t</pre></div></div><div class="top"><p class="src"><a name="v:telePi" class="def">telePi</a> :: <a href="Agda-Syntax-Internal.html#t:Telescope">Telescope</a> -> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-Syntax-Internal.html#t:Type">Type</a><a href="src/Agda-TypeChecking-Substitute.html#telePi" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:telePi_" class="def">telePi_</a> :: <a href="Agda-Syntax-Internal.html#t:Telescope">Telescope</a> -> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-Syntax-Internal.html#t:Type">Type</a><a href="src/Agda-TypeChecking-Substitute.html#telePi_" class="link">Source</a></p><div class="doc"><p>Everything will be a pi.
</p></div></div><div class="top"><p class="src"><a name="v:teleLam" class="def">teleLam</a> :: <a href="Agda-Syntax-Internal.html#t:Telescope">Telescope</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a><a href="src/Agda-TypeChecking-Substitute.html#teleLam" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:dLub" class="def">dLub</a> :: <a href="Agda-Syntax-Internal.html#t:Sort">Sort</a> -> <a href="Agda-Syntax-Internal.html#t:Abs">Abs</a> <a href="Agda-Syntax-Internal.html#t:Sort">Sort</a> -> <a href="Agda-Syntax-Internal.html#t:Sort">Sort</a><a href="src/Agda-TypeChecking-Substitute.html#dLub" class="link">Source</a></p><div class="doc"><p>Dependent least upper bound, to assign a level to expressions
like <code>forall i -> Set i</code>.
</p><p><code>dLub s1 i.s2 = omega</code> if <code>i</code> appears in the rigid variables of <code>s2</code>.
</p></div></div><div class="top"><p class="src"><a name="v:absApp" class="def">absApp</a> :: <a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> t => <a href="Agda-Syntax-Internal.html#t:Abs">Abs</a> t -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> t<a href="src/Agda-TypeChecking-Substitute.html#absApp" class="link">Source</a></p><div class="doc"><p>Instantiate an abstraction
</p></div></div><div class="top"><p class="src"><a name="v:absBody" class="def">absBody</a> :: <a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> t => <a href="Agda-Syntax-Internal.html#t:Abs">Abs</a> t -> t<a href="src/Agda-TypeChecking-Substitute.html#absBody" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:mkAbs" class="def">mkAbs</a> :: (<a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> a, <a href="Agda-TypeChecking-Free.html#t:Free">Free</a> a) => <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> -> a -> <a href="Agda-Syntax-Internal.html#t:Abs">Abs</a> a<a href="src/Agda-TypeChecking-Substitute.html#mkAbs" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:reAbs" class="def">reAbs</a> :: (<a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> a, <a href="Agda-TypeChecking-Free.html#t:Free">Free</a> a) => <a href="Agda-Syntax-Internal.html#t:Abs">Abs</a> a -> <a href="Agda-Syntax-Internal.html#t:Abs">Abs</a> a<a href="src/Agda-TypeChecking-Substitute.html#reAbs" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:underAbs" class="def">underAbs</a> :: <a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> a => (a -> b -> b) -> a -> <a href="Agda-Syntax-Internal.html#t:Abs">Abs</a> b -> <a href="Agda-Syntax-Internal.html#t:Abs">Abs</a> b<a href="src/Agda-TypeChecking-Substitute.html#underAbs" class="link">Source</a></p><div class="doc"><p><code>underAbs k a b</code> applies <code>k</code> to <code>a</code> and the content of
abstraction <code>b</code> and puts the abstraction back.
<code>a</code> is raised if abstraction was proper such that
at point of application of <code>k</code> and the content of <code>b</code>
are at the same context.
Precondition: <code>a</code> and <code>b</code> are at the same context at call time.
</p></div></div><div class="top"><p class="src"><a name="v:underLambdas" class="def">underLambdas</a> :: <a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> a => <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a> -> (a -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a>) -> a -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a><a href="src/Agda-TypeChecking-Substitute.html#underLambdas" class="link">Source</a></p><div class="doc"><p><code>underLambdas n k a b</code> drops <code>n</code> initial <code><a href="Agda-Syntax-Internal.html#v:Lam">Lam</a></code>s from <code>b</code>,
performs operation <code>k</code> on <code>a</code> and the body of <code>b</code>,
and puts the <code><a href="Agda-Syntax-Internal.html#v:Lam">Lam</a></code>s back. <code>a</code> is raised correctly
according to the number of abstractions.
</p></div></div><div class="top"><p class="src"><a name="v:sLub" class="def">sLub</a> :: <a href="Agda-Syntax-Internal.html#t:Sort">Sort</a> -> <a href="Agda-Syntax-Internal.html#t:Sort">Sort</a> -> <a href="Agda-Syntax-Internal.html#t:Sort">Sort</a><a href="src/Agda-TypeChecking-Substitute.html#sLub" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:lvlView" class="def">lvlView</a> :: <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-Syntax-Internal.html#t:Level">Level</a><a href="src/Agda-TypeChecking-Substitute.html#lvlView" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:levelMax" class="def">levelMax</a> :: [<a href="Agda-Syntax-Internal.html#t:PlusLevel">PlusLevel</a>] -> <a href="Agda-Syntax-Internal.html#t:Level">Level</a><a href="src/Agda-TypeChecking-Substitute.html#levelMax" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:sortTm" class="def">sortTm</a> :: <a href="Agda-Syntax-Internal.html#t:Sort">Sort</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a><a href="src/Agda-TypeChecking-Substitute.html#sortTm" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:levelSort" class="def">levelSort</a> :: <a href="Agda-Syntax-Internal.html#t:Level">Level</a> -> <a href="Agda-Syntax-Internal.html#t:Sort">Sort</a><a href="src/Agda-TypeChecking-Substitute.html#levelSort" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:levelTm" class="def">levelTm</a> :: <a href="Agda-Syntax-Internal.html#t:Level">Level</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a><a href="src/Agda-TypeChecking-Substitute.html#levelTm" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:unLevelAtom" class="def">unLevelAtom</a> :: <a href="Agda-Syntax-Internal.html#t:LevelAtom">LevelAtom</a> -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a><a href="src/Agda-TypeChecking-Substitute.html#unLevelAtom" 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>
