<!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-2.3.2.1: A dependently typed functional programming language and proof assistant (Index - U)</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();};
//]]>
</script></head><body><div id="package-header"><ul class="links" id="page-menu"><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="alphabet"><ul><li><a href="doc-index-A.html">A</a></li><li><a href="doc-index-B.html">B</a></li><li><a href="doc-index-C.html">C</a></li><li><a href="doc-index-D.html">D</a></li><li><a href="doc-index-E.html">E</a></li><li><a href="doc-index-F.html">F</a></li><li><a href="doc-index-G.html">G</a></li><li><a href="doc-index-H.html">H</a></li><li><a href="doc-index-I.html">I</a></li><li><a href="doc-index-J.html">J</a></li><li><a href="doc-index-K.html">K</a></li><li><a href="doc-index-L.html">L</a></li><li><a href="doc-index-M.html">M</a></li><li><a href="doc-index-N.html">N</a></li><li><a href="doc-index-O.html">O</a></li><li><a href="doc-index-P.html">P</a></li><li><a href="doc-index-Q.html">Q</a></li><li><a href="doc-index-R.html">R</a></li><li><a href="doc-index-S.html">S</a></li><li><a href="doc-index-T.html">T</a></li><li><a href="doc-index-U.html">U</a></li><li><a href="doc-index-V.html">V</a></li><li><a href="doc-index-W.html">W</a></li><li><a href="doc-index-X.html">X</a></li><li><a href="doc-index-Y.html">Y</a></li><li><a href="doc-index-Z.html">Z</a></li><li><a href="doc-index-58.html">:</a></li><li><a href="doc-index-33.html">!</a></li><li><a href="doc-index-36.html">$</a></li><li><a href="doc-index-38.html">&</a></li><li><a href="doc-index-43.html">+</a></li><li><a href="doc-index-46.html">.</a></li><li><a href="doc-index-47.html">/</a></li><li><a href="doc-index-60.html"><</a></li><li><a href="doc-index-61.html">=</a></li><li><a href="doc-index-62.html">></a></li><li><a href="doc-index-124.html">|</a></li><li><a href="doc-index-45.html">-</a></li><li><a href="doc-index-All.html">All</a></li></ul></div><div id="index"><p class="caption">Index - U</p><table><tr><td class="src">U</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:U">Agda.TypeChecking.Rules.LHS.Unify</a></td></tr><tr><td class="src">UId</td><td class="module"><a href="Agda-Auto-Syntax.html#t:UId">Agda.Auto.Syntax</a></td></tr><tr><td class="src">umodifyIORef</td><td class="module"><a href="Agda-Auto-NarrowingSearch.html#v:umodifyIORef">Agda.Auto.NarrowingSearch</a></td></tr><tr><td class="src">unAbs</td><td class="module"><a href="Agda-Syntax-Internal.html#v:unAbs">Agda.Syntax.Internal</a></td></tr><tr><td class="src">unAmbQ</td><td class="module"><a href="Agda-Syntax-Abstract-Name.html#v:unAmbQ">Agda.Syntax.Abstract.Name</a>, Agda.Syntax.Internal, Agda.Syntax.Abstract</td></tr><tr><td class="src">unAppView</td><td class="module"><a href="Agda-Syntax-Abstract-Views.html#v:unAppView">Agda.Syntax.Abstract.Views</a></td></tr><tr><td class="src">unArg</td><td class="module"><a href="Agda-Syntax-Common.html#v:unArg">Agda.Syntax.Common</a></td></tr><tr><td class="src">UnBlock</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:UnBlock">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">unblockedTester</td><td class="module"><a href="Agda-TypeChecking-MetaVars.html#v:unblockedTester">Agda.TypeChecking.MetaVars</a></td></tr><tr><td class="src">unCommandM</td><td class="module"><a href="Agda-Interaction-InteractionTop.html#v:unCommandM">Agda.Interaction.InteractionTop</a></td></tr><tr><td class="src">unConName</td><td class="module"><a href="Agda-TypeChecking-Test-Generators.html#v:unConName">Agda.TypeChecking.Test.Generators</a></td></tr><tr><td class="src">uncons</td><td class="module"><a href="Agda-Utils-List.html#v:uncons">Agda.Utils.List</a></td></tr><tr><td class="src">uncurry3</td><td class="module"><a href="Agda-Utils-Tuple.html#v:uncurry3">Agda.Utils.Tuple</a></td></tr><tr><td class="src">uncurry4</td><td class="module"><a href="Agda-Utils-Tuple.html#v:uncurry4">Agda.Utils.Tuple</a></td></tr><tr><td class="src">unDeepSizeView</td><td class="module"><a href="Agda-TypeChecking-Monad-SizedTypes.html#v:unDeepSizeView">Agda.TypeChecking.Monad.SizedTypes</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">undef</td><td class="module"><a href="Agda-Compiler-JS-Parser.html#v:undef">Agda.Compiler.JS.Parser</a></td></tr><tr><td class="src">Undefined</td><td class="module"><a href="Agda-Compiler-JS-Syntax.html#v:Undefined">Agda.Compiler.JS.Syntax</a></td></tr><tr><td class="src">unDefName</td><td class="module"><a href="Agda-TypeChecking-Test-Generators.html#v:unDefName">Agda.TypeChecking.Test.Generators</a></td></tr><tr><td class="src">underAbs</td><td class="module"><a href="Agda-TypeChecking-Substitute.html#v:underAbs">Agda.TypeChecking.Substitute</a></td></tr><tr><td class="src">underAbstraction</td><td class="module"><a href="Agda-TypeChecking-Monad-Context.html#v:underAbstraction">Agda.TypeChecking.Monad.Context</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">underAbstraction_</td><td class="module"><a href="Agda-TypeChecking-Monad-Context.html#v:underAbstraction_">Agda.TypeChecking.Monad.Context</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">UnderInf</td><td class="module"><a href="Agda-TypeChecking-Positivity.html#v:UnderInf">Agda.TypeChecking.Positivity</a></td></tr><tr><td class="src">underLambdas</td><td class="module"><a href="Agda-TypeChecking-Substitute.html#v:underLambdas">Agda.TypeChecking.Substitute</a></td></tr><tr><td class="src">Underscore</td><td> </td></tr><tr><td class="alt">1 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:Underscore">Agda.Syntax.Concrete</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:Underscore">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">underscore</td><td class="module"><a href="Agda-Syntax-Concrete-Pretty.html#v:underscore">Agda.Syntax.Concrete.Pretty</a></td></tr><tr><td class="src">Undo</td><td class="module"><a href="Agda-Auto-NarrowingSearch.html#t:Undo">Agda.Auto.NarrowingSearch</a></td></tr><tr><td class="src">unDom</td><td class="module"><a href="Agda-Syntax-Common.html#v:unDom">Agda.Syntax.Common</a></td></tr><tr><td class="src">unEl</td><td class="module"><a href="Agda-Syntax-Internal.html#v:unEl">Agda.Syntax.Internal</a></td></tr><tr><td class="src">unequal</td><td class="module"><a href="Agda-Auto-Typecheck.html#v:unequal">Agda.Auto.Typecheck</a></td></tr><tr><td class="src">UnequalBecauseOfUniverseConflict</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:UnequalBecauseOfUniverseConflict">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">UnequalHiding</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:UnequalHiding">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">UnequalLevel</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:UnequalLevel">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">UnequalRelevance</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:UnequalRelevance">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">unequals</td><td class="module"><a href="Agda-Auto-Typecheck.html#v:unequals">Agda.Auto.Typecheck</a></td></tr><tr><td class="src">UnequalSorts</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:UnequalSorts">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">UnequalTelescopes</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:UnequalTelescopes">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">UnequalTerms</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:UnequalTerms">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">UnequalTypes</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:UnequalTypes">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">unescape</td><td class="module"><a href="Agda-Compiler-JS-Pretty.html#v:unescape">Agda.Compiler.JS.Pretty</a></td></tr><tr><td class="src">unescapes</td><td class="module"><a href="Agda-Compiler-JS-Pretty.html#v:unescapes">Agda.Compiler.JS.Pretty</a></td></tr><tr><td class="src">UnexpectedWithPatterns</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:UnexpectedWithPatterns">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">unExprView</td><td class="module"><a href="Agda-Syntax-Concrete-Operators-Parser.html#v:unExprView">Agda.Syntax.Concrete.Operators.Parser</a></td></tr><tr><td class="src">unflattenTel</td><td class="module"><a href="Agda-TypeChecking-Telescope.html#v:unflattenTel">Agda.TypeChecking.Telescope</a></td></tr><tr><td class="src">unfold</td><td class="module"><a href="Agda-TypeChecking-MetaVars-Occurs.html#v:unfold">Agda.TypeChecking.MetaVars.Occurs</a></td></tr><tr><td class="src">unfoldCorecursion</td><td class="module"><a href="Agda-TypeChecking-CompiledClause-Match.html#v:unfoldCorecursion">Agda.TypeChecking.CompiledClause.Match</a></td></tr><tr><td class="src">unfoldDefinition</td><td class="module"><a href="Agda-TypeChecking-Reduce.html#v:unfoldDefinition">Agda.TypeChecking.Reduce</a></td></tr><tr><td class="src">UnfoldStrategy</td><td class="module"><a href="Agda-TypeChecking-MetaVars-Occurs.html#t:UnfoldStrategy">Agda.TypeChecking.MetaVars.Occurs</a></td></tr><tr><td class="src">unfreezeMetas</td><td class="module"><a href="Agda-TypeChecking-Monad-MetaVars.html#v:unfreezeMetas">Agda.TypeChecking.Monad.MetaVars</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">unGraph</td><td class="module"><a href="Agda-Utils-Graph.html#v:unGraph">Agda.Utils.Graph</a></td></tr><tr><td class="src">unguardedRecord</td><td class="module"><a href="Agda-TypeChecking-Records.html#v:unguardedRecord">Agda.TypeChecking.Records</a></td></tr><tr><td class="src">uniConstr</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:uniConstr">Agda.TypeChecking.Rules.LHS.Unify</a></td></tr><tr><td class="src">Unifiable</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unifiable">Agda.TypeChecking.Rules.LHS.Unify</a></td></tr><tr><td class="src">unifiable</td><td class="module"><a href="Agda-Compiler-Epic-Injection.html#v:unifiable">Agda.Compiler.Epic.Injection</a></td></tr><tr><td class="src">UnificationResult</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:UnificationResult">Agda.TypeChecking.Rules.LHS.Unify</a></td></tr><tr><td class="src">Unifies</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:Unifies">Agda.TypeChecking.Rules.LHS.Unify</a></td></tr><tr><td class="src">Unify</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify">Agda.TypeChecking.Rules.LHS.Unify</a></td></tr><tr><td class="src">unify</td><td class="module"><a href="Agda-Compiler-Epic-Injection.html#v:unify">Agda.Compiler.Epic.Injection</a></td></tr><tr><td class="src">UnifyEnv</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:UnifyEnv">Agda.TypeChecking.Rules.LHS.Unify</a></td></tr><tr><td class="src">UnifyException</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:UnifyException">Agda.TypeChecking.Rules.LHS.Unify</a></td></tr><tr><td class="src">unifyexp</td><td class="module"><a href="Agda-Auto-CaseSplit.html#v:unifyexp">Agda.Auto.CaseSplit</a></td></tr><tr><td class="src">unifyI</td><td class="module"><a href="Agda-Compiler-Epic-Forcing.html#v:unifyI">Agda.Compiler.Epic.Forcing</a></td></tr><tr><td class="src">unifyIndices</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:unifyIndices">Agda.TypeChecking.Rules.LHS.Unify</a></td></tr><tr><td class="src">unifyIndices_</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:unifyIndices_">Agda.TypeChecking.Rules.LHS.Unify</a></td></tr><tr><td class="src">UnifyMayPostpone</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:UnifyMayPostpone">Agda.TypeChecking.Rules.LHS.Unify</a></td></tr><tr><td class="src">UnifyOutput</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:UnifyOutput">Agda.TypeChecking.Rules.LHS.Unify</a></td></tr><tr><td class="src">unifyPointers</td><td class="module"><a href="Agda-TypeChecking-Conversion.html#v:unifyPointers">Agda.TypeChecking.Conversion</a></td></tr><tr><td class="src">UnifyState</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:UnifyState">Agda.TypeChecking.Rules.LHS.Unify</a></td></tr><tr><td class="src">UninstantiatedDotPattern</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:UninstantiatedDotPattern">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">UninstantiatedModule</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:UninstantiatedModule">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">union</td><td> </td></tr><tr><td class="alt">1 (Function)</td><td class="module"><a href="Agda-Utils-VarSet.html#v:union">Agda.Utils.VarSet</a></td></tr><tr><td class="alt">2 (Function)</td><td class="module">Agda.Utils.HashMap</td></tr><tr><td class="alt">3 (Function)</td><td class="module"><a href="Agda-Utils-Trie.html#v:union">Agda.Utils.Trie</a></td></tr><tr><td class="alt">4 (Function)</td><td class="module"><a href="Agda-Termination-CallGraph.html#v:union">Agda.Termination.CallGraph</a></td></tr><tr><td class="alt">5 (Function)</td><td class="module"><a href="Agda-Utils-Graph.html#v:union">Agda.Utils.Graph</a></td></tr><tr><td class="alt">6 (Function)</td><td class="module"><a href="Agda-Compiler-JS-Substitution.html#v:union">Agda.Compiler.JS.Substitution</a></td></tr><tr><td class="src">unionConstraints</td><td class="module"><a href="Agda-Compiler-Epic-Injection.html#v:unionConstraints">Agda.Compiler.Epic.Injection</a></td></tr><tr><td class="src">unions</td><td> </td></tr><tr><td class="alt">1 (Function)</td><td class="module"><a href="Agda-Utils-VarSet.html#v:unions">Agda.Utils.VarSet</a></td></tr><tr><td class="alt">2 (Function)</td><td class="module">Agda.Utils.HashMap</td></tr><tr><td class="alt">3 (Function)</td><td class="module"><a href="Agda-Utils-Graph.html#v:unions">Agda.Utils.Graph</a></td></tr><tr><td class="src">unionSignatures</td><td class="module"><a href="Agda-TypeChecking-Monad-Signature.html#v:unionSignatures">Agda.TypeChecking.Monad.Signature</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">unionWith</td><td class="module">Agda.Utils.HashMap</td></tr><tr><td class="src">unionWithM</td><td class="module"><a href="Agda-Utils-Map.html#v:unionWithM">Agda.Utils.Map</a></td></tr><tr><td class="src">uniqBy</td><td class="module"><a href="Agda-Utils-List.html#v:uniqBy">Agda.Utils.List</a></td></tr><tr><td class="src">uniSub</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:uniSub">Agda.TypeChecking.Rules.LHS.Unify</a></td></tr><tr><td class="src">UNIT</td><td class="module"><a href="Agda-Compiler-Epic-AuxAST.html#v:UNIT">Agda.Compiler.Epic.AuxAST</a></td></tr><tr><td class="src">univar</td><td class="module"><a href="Agda-Auto-SearchControl.html#v:univar">Agda.Auto.SearchControl</a></td></tr><tr><td class="src">Unknown</td><td class="module"><a href="Agda-TypeChecking-Positivity.html#v:Unknown">Agda.TypeChecking.Positivity</a></td></tr><tr><td class="src">unknown</td><td class="module"><a href="Agda-Termination-CallGraph.html#v:unknown">Agda.Termination.CallGraph</a></td></tr><tr><td class="src">UnknownName</td><td class="module"><a href="Agda-Syntax-Scope-Monad.html#v:UnknownName">Agda.Syntax.Scope.Monad</a></td></tr><tr><td class="src">UnknownNamesInFixityDecl</td><td class="module"><a href="Agda-Syntax-Concrete-Definitions.html#v:UnknownNamesInFixityDecl">Agda.Syntax.Concrete.Definitions</a></td></tr><tr><td class="src">UnknownSort</td><td class="module"><a href="Agda-Auto-Syntax.html#v:UnknownSort">Agda.Auto.Syntax</a></td></tr><tr><td class="src">unlessM</td><td class="module"><a href="Agda-Utils-Monad.html#v:unlessM">Agda.Utils.Monad</a></td></tr><tr><td class="src">unless_</td><td class="module"><a href="Agda-Utils-Monad.html#v:unless_">Agda.Utils.Monad</a></td></tr><tr><td class="src">unLevel</td><td class="module"><a href="Agda-TypeChecking-Level.html#v:unLevel">Agda.TypeChecking.Level</a></td></tr><tr><td class="src">unLevelAtom</td><td class="module"><a href="Agda-TypeChecking-Substitute.html#v:unLevelAtom">Agda.TypeChecking.Substitute</a></td></tr><tr><td class="src">unlistenToMeta</td><td class="module"><a href="Agda-TypeChecking-Monad-MetaVars.html#v:unlistenToMeta">Agda.TypeChecking.Monad.MetaVars</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">unLvl</td><td class="module"><a href="Agda-TypeChecking-Primitive.html#v:unLvl">Agda.TypeChecking.Primitive</a></td></tr><tr><td class="src">unMaxView</td><td class="module"><a href="Agda-TypeChecking-Monad-SizedTypes.html#v:unMaxView">Agda.TypeChecking.Monad.SizedTypes</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">unnamed</td><td class="module"><a href="Agda-Syntax-Common.html#v:unnamed">Agda.Syntax.Common</a></td></tr><tr><td class="src">unNat</td><td class="module"><a href="Agda-TypeChecking-Primitive.html#v:unNat">Agda.TypeChecking.Primitive</a></td></tr><tr><td class="src">unNoType</td><td class="module"><a href="Agda-TypeChecking-Test-Generators.html#v:unNoType">Agda.TypeChecking.Test.Generators</a></td></tr><tr><td class="src">unqhname</td><td class="module"><a href="Agda-Compiler-MAlonzo-Misc.html#v:unqhname">Agda.Compiler.MAlonzo.Misc</a></td></tr><tr><td class="src">unqname</td><td class="module"><a href="Agda-Compiler-Epic-CompileState.html#v:unqname">Agda.Compiler.Epic.CompileState</a></td></tr><tr><td class="src">unqualify</td><td class="module"><a href="Agda-Syntax-Concrete-Name.html#v:unqualify">Agda.Syntax.Concrete.Name</a>, Agda.Syntax.Concrete</td></tr><tr><td class="src">Unquote</td><td> </td></tr><tr><td class="alt">1 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:Unquote">Agda.Syntax.Concrete</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:Unquote">Agda.Syntax.Abstract</a></td></tr><tr><td class="alt">3 (Type/Class)</td><td class="module"><a href="Agda-TypeChecking-Quote.html#t:Unquote">Agda.TypeChecking.Quote</a></td></tr><tr><td class="src">unquote</td><td class="module"><a href="Agda-TypeChecking-Quote.html#v:unquote">Agda.TypeChecking.Quote</a></td></tr><tr><td class="src">unquoteFailed</td><td class="module"><a href="Agda-TypeChecking-Quote.html#v:unquoteFailed">Agda.TypeChecking.Quote</a></td></tr><tr><td class="src">unquoteFailedGeneric</td><td class="module"><a href="Agda-TypeChecking-Quote.html#v:unquoteFailedGeneric">Agda.TypeChecking.Quote</a></td></tr><tr><td class="src">unquoteH</td><td class="module"><a href="Agda-TypeChecking-Quote.html#v:unquoteH">Agda.TypeChecking.Quote</a></td></tr><tr><td class="src">unquoteN</td><td class="module"><a href="Agda-TypeChecking-Quote.html#v:unquoteN">Agda.TypeChecking.Quote</a></td></tr><tr><td class="src">UnreachableClauses</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:UnreachableClauses">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">UnreducedLevel</td><td class="module"><a href="Agda-Syntax-Internal.html#v:UnreducedLevel">Agda.Syntax.Internal</a></td></tr><tr><td class="src">unsafeCoerceMod</td><td class="module"><a href="Agda-Compiler-MAlonzo-Misc.html#v:unsafeCoerceMod">Agda.Compiler.MAlonzo.Misc</a></td></tr><tr><td class="src">unsafePragmaOptions</td><td class="module"><a href="Agda-Interaction-Options.html#v:unsafePragmaOptions">Agda.Interaction.Options</a></td></tr><tr><td class="src">unScope</td><td class="module"><a href="Agda-TypeChecking-Rules-Term.html#v:unScope">Agda.TypeChecking.Rules.Term</a></td></tr><tr><td class="src">unSizedList</td><td class="module"><a href="Agda-TypeChecking-Test-Generators.html#v:unSizedList">Agda.TypeChecking.Test.Generators</a></td></tr><tr><td class="src">unSizeView</td><td class="module"><a href="Agda-TypeChecking-Monad-SizedTypes.html#v:unSizeView">Agda.TypeChecking.Monad.SizedTypes</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">UnsolvedConstraint</td><td class="module"><a href="Agda-Interaction-Highlighting-Precise.html#v:UnsolvedConstraint">Agda.Interaction.Highlighting.Precise</a></td></tr><tr><td class="src">UnsolvedConstraints</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:UnsolvedConstraints">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">unsolvedConstraints</td><td class="module"><a href="Agda-TypeChecking-Errors.html#v:unsolvedConstraints">Agda.TypeChecking.Errors</a></td></tr><tr><td class="src">UnsolvedMeta</td><td class="module"><a href="Agda-Interaction-Highlighting-Precise.html#v:UnsolvedMeta">Agda.Interaction.Highlighting.Precise</a></td></tr><tr><td class="src">UnsolvedMetas</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:UnsolvedMetas">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">unsolvedMetaVariables</td><td class="module"><a href="Agda-TypeChecking-Errors.html#v:unsolvedMetaVariables">Agda.TypeChecking.Errors</a></td></tr><tr><td class="src">unStr</td><td class="module"><a href="Agda-TypeChecking-Primitive.html#v:unStr">Agda.TypeChecking.Primitive</a></td></tr><tr><td class="src">unTCM</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:unTCM">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">unUnify</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:unUnify">Agda.TypeChecking.Rules.LHS.Unify</a></td></tr><tr><td class="src">unusableRelevance</td><td class="module"><a href="Agda-TypeChecking-Irrelevance.html#v:unusableRelevance">Agda.TypeChecking.Irrelevance</a></td></tr><tr><td class="src">Unused</td><td> </td></tr><tr><td class="alt">1 (Data Constructor)</td><td class="module"><a href="Agda-TypeChecking-Free.html#v:Unused">Agda.TypeChecking.Free</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:Unused">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">UnusedArg</td><td class="module"><a href="Agda-Syntax-Common.html#v:UnusedArg">Agda.Syntax.Common</a></td></tr><tr><td class="src">UnusedVariableInPatternSynonym</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:UnusedVariableInPatternSynonym">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">unusedVars</td><td class="module"><a href="Agda-TypeChecking-Free.html#v:unusedVars">Agda.TypeChecking.Free</a></td></tr><tr><td class="src">unVarName</td><td class="module"><a href="Agda-TypeChecking-Test-Generators.html#v:unVarName">Agda.TypeChecking.Test.Generators</a></td></tr><tr><td class="src">unwrap</td><td class="module"><a href="Agda-Compiler-MAlonzo-Pretty.html#v:unwrap">Agda.Compiler.MAlonzo.Pretty</a></td></tr><tr><td class="src">unYesType</td><td class="module"><a href="Agda-TypeChecking-Test-Generators.html#v:unYesType">Agda.TypeChecking.Test.Generators</a></td></tr><tr><td class="src">unzip</td><td class="module"><a href="Agda-Utils-Map.html#v:unzip">Agda.Utils.Map</a></td></tr><tr><td class="src">unzip3</td><td class="module"><a href="Agda-Utils-Map.html#v:unzip3">Agda.Utils.Map</a></td></tr><tr><td class="src">unzipMaybe</td><td class="module"><a href="Agda-Utils-Maybe.html#v:unzipMaybe">Agda.Utils.Maybe</a></td></tr><tr><td class="src">updateDefArgOccurrences</td><td class="module"><a href="Agda-TypeChecking-Monad-Signature.html#v:updateDefArgOccurrences">Agda.TypeChecking.Monad.Signature</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">updateDefCompiledRep</td><td class="module"><a href="Agda-TypeChecking-Monad-Signature.html#v:updateDefCompiledRep">Agda.TypeChecking.Monad.Signature</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">updateDefinition</td><td class="module"><a href="Agda-TypeChecking-Monad-Signature.html#v:updateDefinition">Agda.TypeChecking.Monad.Signature</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">updateDefPolarity</td><td class="module"><a href="Agda-TypeChecking-Monad-Signature.html#v:updateDefPolarity">Agda.TypeChecking.Monad.Signature</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">updateDefType</td><td class="module"><a href="Agda-TypeChecking-Monad-Signature.html#v:updateDefType">Agda.TypeChecking.Monad.Signature</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">updateLast</td><td class="module"><a href="Agda-Utils-List.html#v:updateLast">Agda.Utils.List</a></td></tr><tr><td class="src">updateMeta</td><td class="module"><a href="Agda-TypeChecking-MetaVars.html#v:updateMeta">Agda.TypeChecking.MetaVars</a></td></tr><tr><td class="src">updateMetaVar</td><td class="module"><a href="Agda-TypeChecking-Monad-MetaVars.html#v:updateMetaVar">Agda.TypeChecking.Monad.MetaVars</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">updateMetaVarRange</td><td class="module"><a href="Agda-TypeChecking-Monad-MetaVars.html#v:updateMetaVarRange">Agda.TypeChecking.Monad.MetaVars</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">updateNamedArg</td><td class="module"><a href="Agda-Syntax-Common.html#v:updateNamedArg">Agda.Syntax.Common</a></td></tr><tr><td class="src">updateProblemRest</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-ProblemRest.html#v:updateProblemRest">Agda.TypeChecking.Rules.LHS.ProblemRest</a></td></tr><tr><td class="src">updateProblemRest_</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-ProblemRest.html#v:updateProblemRest_">Agda.TypeChecking.Rules.LHS.ProblemRest</a></td></tr><tr><td class="src">updatePtr</td><td class="module"><a href="Agda-Utils-Pointer.html#v:updatePtr">Agda.Utils.Pointer</a>, Agda.Syntax.Internal</td></tr><tr><td class="src">updatePtrM</td><td class="module"><a href="Agda-Utils-Pointer.html#v:updatePtrM">Agda.Utils.Pointer</a>, Agda.Syntax.Internal</td></tr><tr><td class="src">updateShared</td><td class="module"><a href="Agda-Syntax-Internal.html#v:updateShared">Agda.Syntax.Internal</a></td></tr><tr><td class="src">updateSharedFM</td><td class="module"><a href="Agda-Syntax-Internal.html#v:updateSharedFM">Agda.Syntax.Internal</a></td></tr><tr><td class="src">updateSharedM</td><td class="module"><a href="Agda-Syntax-Internal.html#v:updateSharedM">Agda.Syntax.Internal</a></td></tr><tr><td class="src">updateSharedTerm</td><td class="module"><a href="Agda-TypeChecking-Monad-Sharing.html#v:updateSharedTerm">Agda.TypeChecking.Monad.Sharing</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">updateSharedTermF</td><td class="module"><a href="Agda-TypeChecking-Monad-Sharing.html#v:updateSharedTermF">Agda.TypeChecking.Monad.Sharing</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">updateSharedTermT</td><td class="module"><a href="Agda-TypeChecking-Monad-Sharing.html#v:updateSharedTermT">Agda.TypeChecking.Monad.Sharing</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">updateTheDef</td><td class="module"><a href="Agda-TypeChecking-Monad-Signature.html#v:updateTheDef">Agda.TypeChecking.Monad.Signature</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">ureadIORef</td><td class="module"><a href="Agda-Auto-NarrowingSearch.html#v:ureadIORef">Agda.Auto.NarrowingSearch</a></td></tr><tr><td class="src">ureadmodifyIORef</td><td class="module"><a href="Agda-Auto-NarrowingSearch.html#v:ureadmodifyIORef">Agda.Auto.NarrowingSearch</a></td></tr><tr><td class="src">UReduce</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:UReduce">Agda.TypeChecking.Rules.LHS.Unify</a></td></tr><tr><td class="src">ureduce</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:ureduce">Agda.TypeChecking.Rules.LHS.Unify</a></td></tr><tr><td class="src">usage</td><td class="module"><a href="Agda-Interaction-Options.html#v:usage">Agda.Interaction.Options</a></td></tr><tr><td class="src">UseBoundNames</td><td> </td></tr><tr><td class="alt">1 (Type/Class)</td><td class="module"><a href="Agda-Syntax-Concrete-Operators.html#t:UseBoundNames">Agda.Syntax.Concrete.Operators</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Concrete-Operators.html#v:UseBoundNames">Agda.Syntax.Concrete.Operators</a></td></tr><tr><td class="src">usedSeed</td><td class="module">Agda.Utils.QuickCheck</td></tr><tr><td class="src">usedSize</td><td class="module">Agda.Utils.QuickCheck</td></tr><tr><td class="src">useInjectivity</td><td class="module"><a href="Agda-TypeChecking-Injectivity.html#v:useInjectivity">Agda.TypeChecking.Injectivity</a></td></tr><tr><td class="src">UselessAbstract</td><td class="module"><a href="Agda-Syntax-Concrete-Definitions.html#v:UselessAbstract">Agda.Syntax.Concrete.Definitions</a></td></tr><tr><td class="src">UselessPrivate</td><td class="module"><a href="Agda-Syntax-Concrete-Definitions.html#v:UselessPrivate">Agda.Syntax.Concrete.Definitions</a></td></tr><tr><td class="src">UseLit</td><td class="module"><a href="Agda-TypeChecking-Test-Generators.html#v:UseLit">Agda.TypeChecking.Test.Generators</a></td></tr><tr><td class="src">useLitChar</td><td class="module"><a href="Agda-TypeChecking-Test-Generators.html#v:useLitChar">Agda.TypeChecking.Test.Generators</a></td></tr><tr><td class="src">UseLiterals</td><td class="module"><a href="Agda-TypeChecking-Test-Generators.html#t:UseLiterals">Agda.TypeChecking.Test.Generators</a></td></tr><tr><td class="src">useLitFloat</td><td class="module"><a href="Agda-TypeChecking-Test-Generators.html#v:useLitFloat">Agda.TypeChecking.Test.Generators</a></td></tr><tr><td class="src">useLitInt</td><td class="module"><a href="Agda-TypeChecking-Test-Generators.html#v:useLitInt">Agda.TypeChecking.Test.Generators</a></td></tr><tr><td class="src">useLitString</td><td class="module"><a href="Agda-TypeChecking-Test-Generators.html#v:useLitString">Agda.TypeChecking.Test.Generators</a></td></tr><tr><td class="src">useNamesFromPattern</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-ProblemRest.html#v:useNamesFromPattern">Agda.TypeChecking.Rules.LHS.ProblemRest</a></td></tr><tr><td class="src">Uses</td><td class="module"><a href="Agda-Compiler-JS-Syntax.html#t:Uses">Agda.Compiler.JS.Syntax</a></td></tr><tr><td class="src">uses</td><td class="module"><a href="Agda-Compiler-JS-Syntax.html#v:uses">Agda.Compiler.JS.Syntax</a></td></tr><tr><td class="src">Using</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:Using">Agda.Syntax.Concrete</a></td></tr><tr><td class="src">UsingOrHiding</td><td class="module"><a href="Agda-Syntax-Concrete.html#t:UsingOrHiding">Agda.Syntax.Concrete</a></td></tr><tr><td class="src">usingOrHiding</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:usingOrHiding">Agda.Syntax.Concrete</a></td></tr><tr><td class="src">USt</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:USt">Agda.TypeChecking.Rules.LHS.Unify</a></td></tr><tr><td class="src">uwriteIORef</td><td class="module"><a href="Agda-Auto-NarrowingSearch.html#v:uwriteIORef">Agda.Auto.NarrowingSearch</a></td></tr></table></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>
