Sophie: ghc-Agda-devel-2.3.2.1-5.fc19 i686

ghc-Agda-devel-2.3.2.1-5.fc19.i686.rpm

<!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 - P)</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">&amp;</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">&lt;</a></li><li><a href="doc-index-61.html">=</a></li><li><a href="doc-index-62.html">&gt;</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 - P</p><table><tr><td class="src">PageMode</td><td class="module">Agda.Utils.Pretty</td></tr><tr><td class="src">Pair</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Type/Class)</td><td class="module"><a href="Agda-Auto-NarrowingSearch.html#t:Pair">Agda.Auto.NarrowingSearch</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-Auto-NarrowingSearch.html#v:Pair">Agda.Auto.NarrowingSearch</a></td></tr><tr><td class="src">pairwiseFilter</td><td class="module"><a href="Agda-Compiler-Epic-Interface.html#v:pairwiseFilter">Agda.Compiler.Epic.Interface</a></td></tr><tr><td class="src">parallelS</td><td class="module"><a href="Agda-TypeChecking-Substitute.html#v:parallelS">Agda.TypeChecking.Substitute</a></td></tr><tr><td class="src">Paren</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:Paren">Agda.Syntax.Concrete</a></td></tr><tr><td class="src">paren</td><td class="module"><a href="Agda-Syntax-Concrete-Operators.html#v:paren">Agda.Syntax.Concrete.Operators</a></td></tr><tr><td class="src">parened</td><td class="module"><a href="Agda-Compiler-JS-Parser.html#v:parened">Agda.Compiler.JS.Parser</a></td></tr><tr><td class="src">ParenP</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:ParenP">Agda.Syntax.Concrete</a></td></tr><tr><td class="src">parens</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Function)</td><td class="module">Agda.Utils.Pretty</td></tr><tr><td class="alt">2 (Function)</td><td class="module"><a href="Agda-TypeChecking-Pretty.html#v:parens">Agda.TypeChecking.Pretty</a></td></tr><tr><td class="src">parens'</td><td class="module"><a href="Agda-Interaction-InteractionTop.html#v:parens-39-">Agda.Interaction.InteractionTop</a></td></tr><tr><td class="src">ParenV</td><td class="module"><a href="Agda-Syntax-Concrete-Operators-Parser.html#v:ParenV">Agda.Syntax.Concrete.Operators.Parser</a></td></tr><tr><td class="src">Parse</td><td class="module"><a href="Agda-Interaction-InteractionTop.html#t:Parse">Agda.Interaction.InteractionTop</a></td></tr><tr><td class="src">parse</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Function)</td><td class="module"><a href="Agda-Utils-ReadP.html#v:parse">Agda.Utils.ReadP</a></td></tr><tr><td class="alt">2 (Function)</td><td class="module"><a href="Agda-Compiler-JS-Parser.html#v:parse">Agda.Compiler.JS.Parser</a></td></tr><tr><td class="alt">3 (Function)</td><td class="module"><a href="Agda-Syntax-Parser-Monad.html#v:parse">Agda.Syntax.Parser.Monad</a></td></tr><tr><td class="alt">4 (Function)</td><td class="module"><a href="Agda-Syntax-Parser.html#v:parse">Agda.Syntax.Parser</a></td></tr><tr><td class="src">parse'</td><td class="module"><a href="Agda-Utils-ReadP.html#v:parse-39-">Agda.Utils.ReadP</a></td></tr><tr><td class="src">parseAndDoAtToplevel</td><td class="module"><a href="Agda-Interaction-InteractionTop.html#v:parseAndDoAtToplevel">Agda.Interaction.InteractionTop</a></td></tr><tr><td class="src">parseApplication</td><td class="module"><a href="Agda-Syntax-Concrete-Operators.html#v:parseApplication">Agda.Syntax.Concrete.Operators</a></td></tr><tr><td class="src">ParseError</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Type/Class)</td><td class="module"><a href="Agda-Syntax-Parser-Monad.html#t:ParseError">Agda.Syntax.Parser.Monad</a>, <a href="Agda-Syntax-Parser.html#t:ParseError">Agda.Syntax.Parser</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Parser-Monad.html#v:ParseError">Agda.Syntax.Parser.Monad</a>, <a href="Agda-Syntax-Parser.html#v:ParseError">Agda.Syntax.Parser</a></td></tr><tr><td class="src">parseError</td><td class="module"><a href="Agda-Syntax-Parser-Monad.html#v:parseError">Agda.Syntax.Parser.Monad</a></td></tr><tr><td class="src">parseErrorAt</td><td class="module"><a href="Agda-Syntax-Parser-Monad.html#v:parseErrorAt">Agda.Syntax.Parser.Monad</a></td></tr><tr><td class="src">parseExpr</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Function)</td><td class="module"><a href="Agda-Interaction-BasicOps.html#v:parseExpr">Agda.Interaction.BasicOps</a></td></tr><tr><td class="alt">2 (Function)</td><td class="module"><a href="Agda-Interaction-CommandLine-CommandLine.html#v:parseExpr">Agda.Interaction.CommandLine.CommandLine</a></td></tr><tr><td class="src">parseExprIn</td><td class="module"><a href="Agda-Interaction-BasicOps.html#v:parseExprIn">Agda.Interaction.BasicOps</a></td></tr><tr><td class="src">ParseFailed</td><td class="module"><a href="Agda-Syntax-Parser-Monad.html#v:ParseFailed">Agda.Syntax.Parser.Monad</a></td></tr><tr><td class="src">parseFile</td><td class="module"><a href="Agda-Syntax-Parser-Monad.html#v:parseFile">Agda.Syntax.Parser.Monad</a></td></tr><tr><td class="src">parseFile'</td><td class="module"><a href="Agda-Syntax-Parser.html#v:parseFile-39-">Agda.Syntax.Parser</a></td></tr><tr><td class="src">ParseFlags</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Type/Class)</td><td class="module"><a href="Agda-Syntax-Parser-Monad.html#t:ParseFlags">Agda.Syntax.Parser.Monad</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Parser-Monad.html#v:ParseFlags">Agda.Syntax.Parser.Monad</a></td></tr><tr><td class="src">parseFlags</td><td class="module"><a href="Agda-Syntax-Parser-Monad.html#v:parseFlags">Agda.Syntax.Parser.Monad</a></td></tr><tr><td class="src">parseInp</td><td class="module"><a href="Agda-Syntax-Parser-Monad.html#v:parseInp">Agda.Syntax.Parser.Monad</a></td></tr><tr><td class="src">parseKeepComments</td><td class="module"><a href="Agda-Syntax-Parser-Monad.html#v:parseKeepComments">Agda.Syntax.Parser.Monad</a></td></tr><tr><td class="src">parseLastPos</td><td class="module"><a href="Agda-Syntax-Parser-Monad.html#v:parseLastPos">Agda.Syntax.Parser.Monad</a></td></tr><tr><td class="src">parseLayout</td><td class="module"><a href="Agda-Syntax-Parser-Monad.html#v:parseLayout">Agda.Syntax.Parser.Monad</a></td></tr><tr><td class="src">parseLexState</td><td class="module"><a href="Agda-Syntax-Parser-Monad.html#v:parseLexState">Agda.Syntax.Parser.Monad</a></td></tr><tr><td class="src">parseLHS</td><td class="module"><a href="Agda-Syntax-Concrete-Operators.html#v:parseLHS">Agda.Syntax.Concrete.Operators</a></td></tr><tr><td class="src">parseLiterate</td><td class="module"><a href="Agda-Syntax-Parser.html#v:parseLiterate">Agda.Syntax.Parser</a></td></tr><tr><td class="src">ParseOk</td><td class="module"><a href="Agda-Syntax-Parser-Monad.html#v:ParseOk">Agda.Syntax.Parser.Monad</a></td></tr><tr><td class="src">parsePat</td><td class="module"><a href="Agda-Syntax-Concrete-Operators.html#v:parsePat">Agda.Syntax.Concrete.Operators</a></td></tr><tr><td class="src">parsePattern</td><td class="module"><a href="Agda-Syntax-Concrete-Operators.html#v:parsePattern">Agda.Syntax.Concrete.Operators</a></td></tr><tr><td class="src">parsePatternSyn</td><td class="module"><a href="Agda-Syntax-Concrete-Operators.html#v:parsePatternSyn">Agda.Syntax.Concrete.Operators</a></td></tr><tr><td class="src">parsePluginOptions</td><td class="module"><a href="Agda-Interaction-Options.html#v:parsePluginOptions">Agda.Interaction.Options</a></td></tr><tr><td class="src">parsePos</td><td class="module"><a href="Agda-Syntax-Parser-Monad.html#v:parsePos">Agda.Syntax.Parser.Monad</a></td></tr><tr><td class="src">parsePosString</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Function)</td><td class="module"><a href="Agda-Syntax-Parser-Monad.html#v:parsePosString">Agda.Syntax.Parser.Monad</a></td></tr><tr><td class="alt">2 (Function)</td><td class="module"><a href="Agda-Syntax-Parser.html#v:parsePosString">Agda.Syntax.Parser</a></td></tr><tr><td class="src">parsePragmaOptions</td><td class="module"><a href="Agda-Interaction-Options.html#v:parsePragmaOptions">Agda.Interaction.Options</a></td></tr><tr><td class="src">parsePrevChar</td><td class="module"><a href="Agda-Syntax-Parser-Monad.html#v:parsePrevChar">Agda.Syntax.Parser.Monad</a></td></tr><tr><td class="src">parsePrevToken</td><td class="module"><a href="Agda-Syntax-Parser-Monad.html#v:parsePrevToken">Agda.Syntax.Parser.Monad</a></td></tr><tr><td class="src">Parser</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Type/Class)</td><td class="module"><a href="Agda-Compiler-JS-Parser.html#t:Parser">Agda.Compiler.JS.Parser</a></td></tr><tr><td class="alt">2 (Type/Class)</td><td class="module"><a href="Agda-Syntax-Parser-Monad.html#t:Parser">Agda.Syntax.Parser.Monad</a></td></tr><tr><td class="alt">3 (Type/Class)</td><td class="module"><a href="Agda-Syntax-Parser.html#t:Parser">Agda.Syntax.Parser</a></td></tr><tr><td class="src">ParseResult</td><td class="module"><a href="Agda-Syntax-Parser-Monad.html#t:ParseResult">Agda.Syntax.Parser.Monad</a></td></tr><tr><td class="src">parseStandardOptions</td><td class="module"><a href="Agda-Interaction-Options.html#v:parseStandardOptions">Agda.Interaction.Options</a></td></tr><tr><td class="src">ParseState</td><td class="module"><a href="Agda-Syntax-Parser-Monad.html#t:ParseState">Agda.Syntax.Parser.Monad</a></td></tr><tr><td class="src">parseToReadsPrec</td><td class="module"><a href="Agda-Interaction-InteractionTop.html#v:parseToReadsPrec">Agda.Interaction.InteractionTop</a></td></tr><tr><td class="src">Partial</td><td class="module"><a href="Agda-Interaction-Highlighting-Generate.html#v:Partial">Agda.Interaction.Highlighting.Generate</a></td></tr><tr><td class="src">partP</td><td class="module"><a href="Agda-Syntax-Concrete-Operators-Parser.html#v:partP">Agda.Syntax.Concrete.Operators.Parser</a></td></tr><tr><td class="src">Pat</td><td class="module"><a href="Agda-Auto-Syntax.html#t:Pat">Agda.Auto.Syntax</a></td></tr><tr><td class="src">patchUpTrailingImplicits</td><td class="module"><a href="Agda-TypeChecking-Rules-Def.html#v:patchUpTrailingImplicits">Agda.TypeChecking.Rules.Def</a></td></tr><tr><td class="src">PatConApp</td><td class="module"><a href="Agda-Auto-Syntax.html#v:PatConApp">Agda.Auto.Syntax</a></td></tr><tr><td class="src">PatExp</td><td class="module"><a href="Agda-Auto-Syntax.html#v:PatExp">Agda.Auto.Syntax</a></td></tr><tr><td class="src">PatInfo</td><td class="module"><a href="Agda-Syntax-Info.html#t:PatInfo">Agda.Syntax.Info</a></td></tr><tr><td class="src">PatName</td><td class="module"><a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:PatName">Agda.Syntax.Translation.ConcreteToAbstract</a></td></tr><tr><td class="src">PatRange</td><td class="module"><a href="Agda-Syntax-Info.html#v:PatRange">Agda.Syntax.Info</a></td></tr><tr><td class="src">pats</td><td class="module"><a href="Agda-Compiler-JS-Case.html#v:pats">Agda.Compiler.JS.Case</a></td></tr><tr><td class="src">PatSource</td><td class="module"><a href="Agda-Syntax-Info.html#v:PatSource">Agda.Syntax.Info</a></td></tr><tr><td class="src">patsToTerms</td><td class="module"><a href="Agda-TypeChecking-With.html#v:patsToTerms">Agda.TypeChecking.With</a></td></tr><tr><td class="src">Patt</td><td class="module"><a href="Agda-Compiler-JS-Case.html#t:Patt">Agda.Compiler.JS.Case</a></td></tr><tr><td class="src">Pattern</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Type/Class)</td><td class="module"><a href="Agda-Syntax-Concrete.html#t:Pattern">Agda.Syntax.Concrete</a></td></tr><tr><td class="alt">2 (Type/Class)</td><td class="module"><a href="Agda-Syntax-Internal.html#t:Pattern">Agda.Syntax.Internal</a></td></tr><tr><td class="alt">3 (Type/Class)</td><td class="module"><a href="Agda-Syntax-Abstract.html#t:Pattern">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">pattern</td><td class="module"><a href="Agda-Compiler-JS-Compiler.html#v:pattern">Agda.Compiler.JS.Compiler</a></td></tr><tr><td class="src">Pattern'</td><td class="module"><a href="Agda-Syntax-Abstract.html#t:Pattern-39-">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">patternAppView</td><td class="module"><a href="Agda-Syntax-Concrete-Operators.html#v:patternAppView">Agda.Syntax.Concrete.Operators</a></td></tr><tr><td class="src">PatternErr</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:PatternErr">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">patternHead</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:patternHead">Agda.Syntax.Concrete</a></td></tr><tr><td class="src">patternNames</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:patternNames">Agda.Syntax.Concrete</a></td></tr><tr><td class="src">patternQNames</td><td class="module"><a href="Agda-Syntax-Concrete-Operators.html#v:patternQNames">Agda.Syntax.Concrete.Operators</a></td></tr><tr><td class="src">Patterns</td><td class="module"><a href="Agda-Syntax-Abstract.html#t:Patterns">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">PatternShadowsConstructor</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:PatternShadowsConstructor">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">PatternSyn</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:PatternSyn">Agda.Syntax.Concrete</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:PatternSyn">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">PatternSynDefn</td><td class="module"><a href="Agda-Syntax-Abstract.html#t:PatternSynDefn">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">PatternSynDefns</td><td class="module"><a href="Agda-Syntax-Abstract.html#t:PatternSynDefns">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">PatternSynName</td><td class="module"><a href="Agda-Syntax-Scope-Base.html#v:PatternSynName">Agda.Syntax.Scope.Base</a></td></tr><tr><td class="src">PatternSynonymArityMismatch</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:PatternSynonymArityMismatch">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">PatternSynP</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:PatternSynP">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">PatternSynResName</td><td class="module"><a href="Agda-Syntax-Scope-Monad.html#v:PatternSynResName">Agda.Syntax.Scope.Monad</a></td></tr><tr><td class="src">patternToExpr</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:patternToExpr">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">patternToTerm</td><td class="module"><a href="Agda-Compiler-Epic-Injection.html#v:patternToTerm">Agda.Compiler.Epic.Injection</a></td></tr><tr><td class="src">patternVars</td><td class="module"><a href="Agda-Syntax-Internal.html#v:patternVars">Agda.Syntax.Internal</a></td></tr><tr><td class="src">patternViolation</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:patternViolation">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">PatVar</td><td class="module"><a href="Agda-Auto-Syntax.html#v:PatVar">Agda.Auto.Syntax</a></td></tr><tr><td class="src">PB</td><td class="module"><a href="Agda-Auto-NarrowingSearch.html#t:PB">Agda.Auto.NarrowingSearch</a></td></tr><tr><td class="src">PBlocked</td><td class="module"><a href="Agda-Auto-NarrowingSearch.html#v:PBlocked">Agda.Auto.NarrowingSearch</a></td></tr><tr><td class="src">pconName</td><td class="module"><a href="Agda-Compiler-MAlonzo-Primitives.html#v:pconName">Agda.Compiler.MAlonzo.Primitives</a></td></tr><tr><td class="src">PConstr</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:PConstr">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">PDoubleBlocked</td><td class="module"><a href="Agda-Auto-NarrowingSearch.html#v:PDoubleBlocked">Agda.Auto.NarrowingSearch</a></td></tr><tr><td class="src">PEConApp</td><td class="module"><a href="Agda-Auto-Typecheck.html#v:PEConApp">Agda.Auto.Typecheck</a></td></tr><tr><td class="src">PENo</td><td class="module"><a href="Agda-Auto-Typecheck.html#v:PENo">Agda.Auto.Typecheck</a></td></tr><tr><td class="src">performKill</td><td class="module"><a href="Agda-TypeChecking-MetaVars-Occurs.html#v:performKill">Agda.TypeChecking.MetaVars.Occurs</a></td></tr><tr><td class="src">Perm</td><td class="module"><a href="Agda-Utils-Permutation.html#v:Perm">Agda.Utils.Permutation</a></td></tr><tr><td class="src">permPicks</td><td class="module"><a href="Agda-Utils-Permutation.html#v:permPicks">Agda.Utils.Permutation</a></td></tr><tr><td class="src">permRange</td><td class="module"><a href="Agda-Utils-Permutation.html#v:permRange">Agda.Utils.Permutation</a></td></tr><tr><td class="src">Permutation</td><td class="module"><a href="Agda-Utils-Permutation.html#t:Permutation">Agda.Utils.Permutation</a></td></tr><tr><td class="src">permute</td><td class="module"><a href="Agda-Utils-Permutation.html#v:permute">Agda.Utils.Permutation</a></td></tr><tr><td class="src">PersistentTCSt</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:PersistentTCSt">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">PersistentTCState</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#t:PersistentTCState">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">PEval</td><td class="module"><a href="Agda-Auto-Typecheck.html#t:PEval">Agda.Auto.Typecheck</a></td></tr><tr><td class="src">pfail</td><td class="module"><a href="Agda-Utils-ReadP.html#v:pfail">Agda.Utils.ReadP</a></td></tr><tr><td class="src">pHidden</td><td class="module"><a href="Agda-Syntax-Concrete-Pretty.html#v:pHidden">Agda.Syntax.Concrete.Pretty</a></td></tr><tr><td class="src">Pi</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Data Constructor)</td><td class="module"><a href="Agda-Auto-Syntax.html#v:Pi">Agda.Auto.Syntax</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:Pi">Agda.Syntax.Concrete</a></td></tr><tr><td class="alt">3 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Internal.html#v:Pi">Agda.Syntax.Internal</a></td></tr><tr><td class="alt">4 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:Pi">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">piAbstractTerm</td><td class="module"><a href="Agda-TypeChecking-Abstract.html#v:piAbstractTerm">Agda.TypeChecking.Abstract</a></td></tr><tr><td class="src">piApply</td><td class="module"><a href="Agda-TypeChecking-Substitute.html#v:piApply">Agda.TypeChecking.Substitute</a></td></tr><tr><td class="src">piApplyM</td><td class="module"><a href="Agda-TypeChecking-Telescope.html#v:piApplyM">Agda.TypeChecking.Telescope</a></td></tr><tr><td class="src">piApplyM'</td><td class="module"><a href="Agda-Compiler-Epic-Forcing.html#v:piApplyM-39-">Agda.Compiler.Epic.Forcing</a></td></tr><tr><td class="src">piBrackets</td><td class="module"><a href="Agda-Syntax-Fixity.html#v:piBrackets">Agda.Syntax.Fixity</a></td></tr><tr><td class="src">pickid</td><td class="module"><a href="Agda-Auto-Typecheck.html#v:pickid">Agda.Auto.Typecheck</a></td></tr><tr><td class="src">piFreq</td><td class="module"><a href="Agda-TypeChecking-Test-Generators.html#v:piFreq">Agda.TypeChecking.Test.Generators</a></td></tr><tr><td class="src">PiHead</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:PiHead">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">PiNotLam</td><td class="module"><a href="Agda-TypeChecking-Rules-Term.html#v:PiNotLam">Agda.TypeChecking.Rules.Term</a></td></tr><tr><td class="src">PiSh</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:PiSh">Agda.TypeChecking.Rules.LHS.Unify</a></td></tr><tr><td class="src">plugHole</td><td class="module"><a href="Agda-Syntax-Internal-Pattern.html#v:plugHole">Agda.Syntax.Internal.Pattern</a></td></tr><tr><td class="src">Plus</td><td class="module"><a href="Agda-Syntax-Internal.html#v:Plus">Agda.Syntax.Internal</a></td></tr><tr><td class="src">PlusLevel</td><td class="module"><a href="Agda-Syntax-Internal.html#t:PlusLevel">Agda.Syntax.Internal</a></td></tr><tr><td class="src">Pn</td><td class="module"><a href="Agda-Syntax-Position.html#v:Pn">Agda.Syntax.Position</a></td></tr><tr><td class="src">point</td><td class="module"><a href="Agda-Utils-Pointed.html#v:point">Agda.Utils.Pointed</a></td></tr><tr><td class="src">Pointed</td><td class="module"><a href="Agda-Utils-Pointed.html#t:Pointed">Agda.Utils.Pointed</a></td></tr><tr><td class="src">pointerChain</td><td class="module"><a href="Agda-Syntax-Internal.html#v:pointerChain">Agda.Syntax.Internal</a></td></tr><tr><td class="src">polarities</td><td class="module"><a href="Agda-TypeChecking-Polarity.html#v:polarities">Agda.TypeChecking.Polarity</a></td></tr><tr><td class="src">Polarity</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#t:Polarity">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">polarity</td><td class="module"><a href="Agda-TypeChecking-Polarity.html#v:polarity">Agda.TypeChecking.Polarity</a></td></tr><tr><td class="src">polFromOcc</td><td class="module"><a href="Agda-TypeChecking-Polarity.html#v:polFromOcc">Agda.TypeChecking.Polarity</a></td></tr><tr><td class="src">pop</td><td class="module"><a href="Agda-Compiler-JS-Case.html#v:pop">Agda.Compiler.JS.Case</a></td></tr><tr><td class="src">popContext</td><td class="module"><a href="Agda-Syntax-Parser-Monad.html#v:popContext">Agda.Syntax.Parser.Monad</a></td></tr><tr><td class="src">popLexState</td><td class="module"><a href="Agda-Syntax-Parser-Monad.html#v:popLexState">Agda.Syntax.Parser.Monad</a></td></tr><tr><td class="src">popMapS</td><td class="module"><a href="Agda-Auto-Convert.html#v:popMapS">Agda.Auto.Convert</a></td></tr><tr><td class="src">posCol</td><td class="module"><a href="Agda-Syntax-Position.html#v:posCol">Agda.Syntax.Position</a></td></tr><tr><td class="src">Position</td><td class="module"><a href="Agda-Syntax-Position.html#t:Position">Agda.Syntax.Position</a></td></tr><tr><td class="src">Position'</td><td class="module"><a href="Agda-Syntax-Position.html#t:Position-39-">Agda.Syntax.Position</a></td></tr><tr><td class="src">positionInvariant</td><td class="module"><a href="Agda-Syntax-Position.html#v:positionInvariant">Agda.Syntax.Position</a></td></tr><tr><td class="src">Positive</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Data Constructor)</td><td class="module">Agda.Utils.QuickCheck</td></tr><tr><td class="alt">2 (Type/Class)</td><td class="module">Agda.Utils.QuickCheck</td></tr><tr><td class="src">positive</td><td class="module"><a href="Agda-Utils-TestHelpers.html#v:positive">Agda.Utils.TestHelpers</a></td></tr><tr><td class="src">positivityCheckEnabled</td><td class="module"><a href="Agda-TypeChecking-Monad-Options.html#v:positivityCheckEnabled">Agda.TypeChecking.Monad.Options</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">posLine</td><td class="module"><a href="Agda-Syntax-Position.html#v:posLine">Agda.Syntax.Position</a></td></tr><tr><td class="src">posPos</td><td class="module"><a href="Agda-Syntax-Position.html#v:posPos">Agda.Syntax.Position</a></td></tr><tr><td class="src">Possibly</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:Possibly">Agda.TypeChecking.Rules.LHS.Unify</a></td></tr><tr><td class="src">postfixP</td><td class="module"><a href="Agda-Syntax-Concrete-Operators-Parser.html#v:postfixP">Agda.Syntax.Concrete.Operators.Parser</a></td></tr><tr><td class="src">postop</td><td class="module"><a href="Agda-Syntax-Concrete-Operators-Parser.html#v:postop">Agda.Syntax.Concrete.Operators.Parser</a></td></tr><tr><td class="src">posToRange</td><td class="module"><a href="Agda-Syntax-Position.html#v:posToRange">Agda.Syntax.Position</a></td></tr><tr><td class="src">PostponedTypeCheckingProblem</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:PostponedTypeCheckingProblem">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">postponeTypeCheckingProblem</td><td class="module"><a href="Agda-TypeChecking-MetaVars.html#v:postponeTypeCheckingProblem">Agda.TypeChecking.MetaVars</a></td></tr><tr><td class="src">postponeTypeCheckingProblem_</td><td class="module"><a href="Agda-TypeChecking-MetaVars.html#v:postponeTypeCheckingProblem_">Agda.TypeChecking.MetaVars</a></td></tr><tr><td class="src">Postulate</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Data Constructor)</td><td class="module"><a href="Agda-Auto-Syntax.html#v:Postulate">Agda.Auto.Syntax</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:Postulate">Agda.Syntax.Concrete</a></td></tr><tr><td class="alt">3 (Data Constructor)</td><td class="module"><a href="Agda-Interaction-Highlighting-Precise.html#v:Postulate">Agda.Interaction.Highlighting.Precise</a></td></tr><tr><td class="src">Pragma</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Type/Class)</td><td class="module"><a href="Agda-Syntax-Concrete.html#t:Pragma">Agda.Syntax.Concrete</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:Pragma">Agda.Syntax.Concrete</a></td></tr><tr><td class="alt">3 (Type/Class)</td><td class="module"><a href="Agda-Syntax-Abstract.html#t:Pragma">Agda.Syntax.Abstract</a></td></tr><tr><td class="alt">4 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:Pragma">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">PragmaOptions</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Type/Class)</td><td class="module"><a href="Agda-Interaction-Options.html#t:PragmaOptions">Agda.Interaction.Options</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-Interaction-Options.html#v:PragmaOptions">Agda.Interaction.Options</a></td></tr><tr><td class="src">pragmaOptions</td><td class="module"><a href="Agda-TypeChecking-Monad-Options.html#v:pragmaOptions">Agda.TypeChecking.Monad.Options</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">Precedence</td><td class="module"><a href="Agda-Syntax-Fixity.html#t:Precedence">Agda.Syntax.Fixity</a></td></tr><tr><td class="src">Pred</td><td class="module"><a href="Agda-TypeChecking-Primitive.html#t:Pred">Agda.TypeChecking.Primitive</a></td></tr><tr><td class="src">Prefix</td><td class="module"><a href="Agda-Utils-List.html#t:Prefix">Agda.Utils.List</a></td></tr><tr><td class="src">prefix</td><td class="module"><a href="Agda-Compiler-JS-Compiler.html#v:prefix">Agda.Compiler.JS.Compiler</a></td></tr><tr><td class="src">PrefixDef</td><td class="module"><a href="Agda-Syntax-Common.html#v:PrefixDef">Agda.Syntax.Common</a></td></tr><tr><td class="src">prefixP</td><td class="module"><a href="Agda-Syntax-Concrete-Operators-Parser.html#v:prefixP">Agda.Syntax.Concrete.Operators.Parser</a></td></tr><tr><td class="src">pRelevance</td><td class="module"><a href="Agda-Syntax-Concrete-Pretty.html#v:pRelevance">Agda.Syntax.Concrete.Pretty</a></td></tr><tr><td class="src">preMeta</td><td class="module"><a href="Agda-Interaction-InteractionTop.html#v:preMeta">Agda.Interaction.InteractionTop</a></td></tr><tr><td class="src">PreOp</td><td class="module"><a href="Agda-Compiler-JS-Syntax.html#v:PreOp">Agda.Compiler.JS.Syntax</a></td></tr><tr><td class="src">preop</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Function)</td><td class="module"><a href="Agda-Compiler-JS-Parser.html#v:preop">Agda.Compiler.JS.Parser</a></td></tr><tr><td class="alt">2 (Function)</td><td class="module"><a href="Agda-Syntax-Concrete-Operators-Parser.html#v:preop">Agda.Syntax.Concrete.Operators.Parser</a></td></tr><tr><td class="src">Pretties</td><td class="module"><a href="Agda-Compiler-JS-Pretty.html#t:Pretties">Agda.Compiler.JS.Pretty</a></td></tr><tr><td class="src">pretties</td><td class="module"><a href="Agda-Compiler-JS-Pretty.html#v:pretties">Agda.Compiler.JS.Pretty</a></td></tr><tr><td class="src">Pretty</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Type/Class)</td><td class="module"><a href="Agda-Utils-Pretty.html#t:Pretty">Agda.Utils.Pretty</a></td></tr><tr><td class="alt">2 (Type/Class)</td><td class="module"><a href="Agda-Compiler-JS-Pretty.html#t:Pretty">Agda.Compiler.JS.Pretty</a></td></tr><tr><td class="src">pretty</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Function)</td><td class="module"><a href="Agda-Utils-Pretty.html#v:pretty">Agda.Utils.Pretty</a></td></tr><tr><td class="alt">2 (Function)</td><td class="module"><a href="Agda-Compiler-JS-Pretty.html#v:pretty">Agda.Compiler.JS.Pretty</a></td></tr><tr><td class="alt">3 (Function)</td><td class="module"><a href="Agda-TypeChecking-Pretty.html#v:pretty">Agda.TypeChecking.Pretty</a></td></tr><tr><td class="src">prettyA</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Function)</td><td class="module"><a href="Agda-Syntax-Abstract-Pretty.html#v:prettyA">Agda.Syntax.Abstract.Pretty</a></td></tr><tr><td class="alt">2 (Function)</td><td class="module"><a href="Agda-TypeChecking-Pretty.html#v:prettyA">Agda.TypeChecking.Pretty</a></td></tr><tr><td class="src">prettyATop</td><td class="module"><a href="Agda-Syntax-Abstract-Pretty.html#v:prettyATop">Agda.Syntax.Abstract.Pretty</a></td></tr><tr><td class="src">prettyBehaviour</td><td class="module"><a href="Agda-Termination-CallGraph.html#v:prettyBehaviour">Agda.Termination.CallGraph</a></td></tr><tr><td class="src">PrettyContext</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Type/Class)</td><td class="module"><a href="Agda-TypeChecking-Pretty.html#t:PrettyContext">Agda.TypeChecking.Pretty</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-TypeChecking-Pretty.html#v:PrettyContext">Agda.TypeChecking.Pretty</a></td></tr><tr><td class="src">prettyContext</td><td class="module"><a href="Agda-Interaction-InteractionTop.html#v:prettyContext">Agda.Interaction.InteractionTop</a></td></tr><tr><td class="src">prettyEpic</td><td class="module"><a href="Agda-Compiler-Epic-Epic.html#v:prettyEpic">Agda.Compiler.Epic.Epic</a></td></tr><tr><td class="src">prettyEpicFun</td><td class="module"><a href="Agda-Compiler-Epic-Epic.html#v:prettyEpicFun">Agda.Compiler.Epic.Epic</a></td></tr><tr><td class="src">prettyError</td><td class="module"><a href="Agda-TypeChecking-Errors.html#v:prettyError">Agda.TypeChecking.Errors</a></td></tr><tr><td class="src">prettyList</td><td class="module"><a href="Agda-TypeChecking-Pretty.html#v:prettyList">Agda.TypeChecking.Pretty</a></td></tr><tr><td class="src">prettyOpApp</td><td class="module"><a href="Agda-Syntax-Concrete-Pretty.html#v:prettyOpApp">Agda.Syntax.Concrete.Pretty</a></td></tr><tr><td class="src">prettyPrec</td><td class="module"><a href="Agda-Utils-Pretty.html#v:prettyPrec">Agda.Utils.Pretty</a></td></tr><tr><td class="src">prettyPrint</td><td class="module"><a href="Agda-Compiler-MAlonzo-Pretty.html#v:prettyPrint">Agda.Compiler.MAlonzo.Pretty</a></td></tr><tr><td class="src">PrettyTCM</td><td class="module"><a href="Agda-TypeChecking-Pretty.html#t:PrettyTCM">Agda.TypeChecking.Pretty</a>, <a href="Agda-TypeChecking-Errors.html#t:PrettyTCM">Agda.TypeChecking.Errors</a></td></tr><tr><td class="src">prettyTCM</td><td class="module"><a href="Agda-TypeChecking-Pretty.html#v:prettyTCM">Agda.TypeChecking.Pretty</a>, <a href="Agda-TypeChecking-Errors.html#v:prettyTCM">Agda.TypeChecking.Errors</a></td></tr><tr><td class="src">prettyTypeOfMeta</td><td class="module"><a href="Agda-Interaction-InteractionTop.html#v:prettyTypeOfMeta">Agda.Interaction.InteractionTop</a></td></tr><tr><td class="src">preUscore</td><td class="module"><a href="Agda-Interaction-InteractionTop.html#v:preUscore">Agda.Interaction.InteractionTop</a></td></tr><tr><td class="src">PreviousInput</td><td class="module"><a href="Agda-Syntax-Parser-Alex.html#t:PreviousInput">Agda.Syntax.Parser.Alex</a></td></tr><tr><td class="src">prFalse</td><td class="module"><a href="Agda-Compiler-Epic-Primitive.html#v:prFalse">Agda.Compiler.Epic.Primitive</a></td></tr><tr><td class="src">Prim</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:Prim">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">primAbstr</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:primAbstr">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">primAgdaDataDef</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primAgdaDataDef">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primAgdaDefinition</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primAgdaDefinition">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primAgdaDefinitionDataConstructor</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primAgdaDefinitionDataConstructor">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primAgdaDefinitionDataDef</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primAgdaDefinitionDataDef">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primAgdaDefinitionFunDef</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primAgdaDefinitionFunDef">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primAgdaDefinitionPostulate</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primAgdaDefinitionPostulate">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primAgdaDefinitionPrimitive</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primAgdaDefinitionPrimitive">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primAgdaDefinitionRecordDef</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primAgdaDefinitionRecordDef">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primAgdaFunDef</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primAgdaFunDef">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primAgdaRecordDef</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primAgdaRecordDef">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primAgdaSort</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primAgdaSort">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primAgdaSortLit</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primAgdaSortLit">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primAgdaSortSet</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primAgdaSortSet">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primAgdaSortUnsupported</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primAgdaSortUnsupported">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primAgdaTerm</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primAgdaTerm">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primAgdaTermCon</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primAgdaTermCon">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primAgdaTermDef</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primAgdaTermDef">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primAgdaTermLam</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primAgdaTermLam">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primAgdaTermPi</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primAgdaTermPi">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primAgdaTermSort</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primAgdaTermSort">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primAgdaTermUnsupported</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primAgdaTermUnsupported">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primAgdaTermVar</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primAgdaTermVar">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primAgdaType</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primAgdaType">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primAgdaTypeEl</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primAgdaTypeEl">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primArg</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primArg">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primArgArg</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primArgArg">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primBody</td><td class="module"><a href="Agda-Compiler-MAlonzo-Primitives.html#v:primBody">Agda.Compiler.MAlonzo.Primitives</a></td></tr><tr><td class="src">primBool</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primBool">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primChar</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primChar">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primClauses</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:primClauses">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">primCompiled</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:primCompiled">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">primCons</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primCons">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primDataConstructors</td><td class="module"><a href="Agda-TypeChecking-Primitive.html#v:primDataConstructors">Agda.TypeChecking.Primitive</a></td></tr><tr><td class="src">Prime</td><td class="module"><a href="Agda-Utils-Suffix.html#v:Prime">Agda.Utils.Suffix</a></td></tr><tr><td class="src">primEquality</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primEquality">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primExpr</td><td class="module"><a href="Agda-Compiler-Epic-Primitive.html#v:primExpr">Agda.Compiler.Epic.Primitive</a></td></tr><tr><td class="src">primFalse</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primFalse">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primFlat</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primFlat">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primFloat</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primFloat">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">PrimFun</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Type/Class)</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#t:PrimFun">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:PrimFun">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">primFun</td><td class="module"><a href="Agda-Compiler-Epic-Primitive.html#v:primFun">Agda.Compiler.Epic.Primitive</a></td></tr><tr><td class="src">primFunArity</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:primFunArity">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">primFunImplementation</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:primFunImplementation">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">primFunName</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:primFunName">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">primHidden</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primHidden">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primHiding</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primHiding">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">PrimImpl</td><td class="module"><a href="Agda-TypeChecking-Primitive.html#v:PrimImpl">Agda.TypeChecking.Primitive</a></td></tr><tr><td class="src">primInf</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primInf">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primInstance</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primInstance">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primInteger</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primInteger">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primIO</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primIO">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primIrrAxiom</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primIrrAxiom">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primIrrelevant</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primIrrelevant">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">Primitive</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:Primitive">Agda.Syntax.Concrete</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-Interaction-Highlighting-Precise.html#v:Primitive">Agda.Interaction.Highlighting.Precise</a></td></tr><tr><td class="alt">3 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:Primitive">Agda.Syntax.Abstract</a></td></tr><tr><td class="alt">4 (Data Constructor)</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:Primitive">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">PrimitiveFunction</td><td class="module"><a href="Agda-Syntax-Concrete-Definitions.html#v:PrimitiveFunction">Agda.Syntax.Concrete.Definitions</a></td></tr><tr><td class="src">primitiveFunctions</td><td class="module"><a href="Agda-TypeChecking-Primitive.html#v:primitiveFunctions">Agda.TypeChecking.Primitive</a></td></tr><tr><td class="src">PrimitiveImpl</td><td class="module"><a href="Agda-TypeChecking-Primitive.html#t:PrimitiveImpl">Agda.TypeChecking.Primitive</a></td></tr><tr><td class="src">PrimitiveType</td><td class="module"><a href="Agda-Interaction-Highlighting-Precise.html#v:PrimitiveType">Agda.Interaction.Highlighting.Precise</a></td></tr><tr><td class="src">primitivise</td><td class="module"><a href="Agda-Compiler-Epic-Primitive.html#v:primitivise">Agda.Compiler.Epic.Primitive</a></td></tr><tr><td class="src">primLevel</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primLevel">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primLevelMax</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primLevelMax">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primLevelSuc</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primLevelSuc">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primLevelZero</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primLevelZero">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primList</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primList">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primName</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:primName">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">primNat</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primNat">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primNatCaseZD</td><td class="module"><a href="Agda-Compiler-Epic-Primitive.html#v:primNatCaseZD">Agda.Compiler.Epic.Primitive</a></td></tr><tr><td class="src">primNatCaseZS</td><td class="module"><a href="Agda-Compiler-Epic-Primitive.html#v:primNatCaseZS">Agda.Compiler.Epic.Primitive</a></td></tr><tr><td class="src">primNatDivSucAux</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primNatDivSucAux">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primNatEquality</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primNatEquality">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primNatLess</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primNatLess">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primNatMinus</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primNatMinus">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primNatModSucAux</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primNatModSucAux">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primNatPlus</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primNatPlus">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primNatTimes</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primNatTimes">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primNil</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primNil">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primQName</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primQName">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primQNameDefinition</td><td class="module"><a href="Agda-TypeChecking-Primitive.html#v:primQNameDefinition">Agda.TypeChecking.Primitive</a></td></tr><tr><td class="src">primQNameType</td><td class="module"><a href="Agda-TypeChecking-Primitive.html#v:primQNameType">Agda.TypeChecking.Primitive</a></td></tr><tr><td class="src">primRefl</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primRefl">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primRelevance</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primRelevance">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primRelevant</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primRelevant">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primSharp</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primSharp">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primSize</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primSize">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primSizeInf</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primSizeInf">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primSizeLt</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primSizeLt">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primSizeMax</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primSizeMax">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primSizeSuc</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primSizeSuc">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primString</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primString">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primSuc</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primSuc">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">PrimTag</td><td class="module"><a href="Agda-Compiler-Epic-Interface.html#v:PrimTag">Agda.Compiler.Epic.Interface</a></td></tr><tr><td class="src">PrimTerm</td><td class="module"><a href="Agda-TypeChecking-Primitive.html#t:PrimTerm">Agda.TypeChecking.Primitive</a></td></tr><tr><td class="src">primTerm</td><td class="module"><a href="Agda-TypeChecking-Primitive.html#v:primTerm">Agda.TypeChecking.Primitive</a></td></tr><tr><td class="src">PrimTF</td><td class="module"><a href="Agda-Compiler-Epic-Primitive.html#v:PrimTF">Agda.Compiler.Epic.Primitive</a></td></tr><tr><td class="src">PrimTransform</td><td class="module"><a href="Agda-Compiler-Epic-Primitive.html#t:PrimTransform">Agda.Compiler.Epic.Primitive</a></td></tr><tr><td class="src">primTrue</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primTrue">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primTrustMe</td><td class="module"><a href="Agda-TypeChecking-Primitive.html#v:primTrustMe">Agda.TypeChecking.Primitive</a></td></tr><tr><td class="src">PrimType</td><td class="module"><a href="Agda-TypeChecking-Primitive.html#t:PrimType">Agda.TypeChecking.Primitive</a></td></tr><tr><td class="src">primType</td><td class="module"><a href="Agda-TypeChecking-Primitive.html#v:primType">Agda.TypeChecking.Primitive</a></td></tr><tr><td class="src">primVisible</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primVisible">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">primZero</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:primZero">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">printErrorInfo</td><td class="module"><a href="Agda-Interaction-Highlighting-Generate.html#v:printErrorInfo">Agda.Interaction.Highlighting.Generate</a></td></tr><tr><td class="src">printHighlightingInfo</td><td class="module"><a href="Agda-Interaction-Highlighting-Generate.html#v:printHighlightingInfo">Agda.Interaction.Highlighting.Generate</a></td></tr><tr><td class="src">printTestCase</td><td class="module">Agda.Utils.QuickCheck</td></tr><tr><td class="src">printUnsolvedInfo</td><td class="module"><a href="Agda-Interaction-Highlighting-Generate.html#v:printUnsolvedInfo">Agda.Interaction.Highlighting.Generate</a></td></tr><tr><td class="src">printUsage</td><td class="module"><a href="Agda-Main.html#v:printUsage">Agda.Main</a></td></tr><tr><td class="src">printVersion</td><td class="module"><a href="Agda-Main.html#v:printVersion">Agda.Main</a></td></tr><tr><td class="src">Prio</td><td class="module"><a href="Agda-Auto-NarrowingSearch.html#t:Prio">Agda.Auto.NarrowingSearch</a></td></tr><tr><td class="src">prioAbsurdLambda</td><td class="module"><a href="Agda-Auto-SearchControl.html#v:prioAbsurdLambda">Agda.Auto.SearchControl</a></td></tr><tr><td class="src">prioCompareArgList</td><td class="module"><a href="Agda-Auto-SearchControl.html#v:prioCompareArgList">Agda.Auto.SearchControl</a></td></tr><tr><td class="src">prioCompBeta</td><td class="module"><a href="Agda-Auto-SearchControl.html#v:prioCompBeta">Agda.Auto.SearchControl</a></td></tr><tr><td class="src">prioCompBetaStructured</td><td class="module"><a href="Agda-Auto-SearchControl.html#v:prioCompBetaStructured">Agda.Auto.SearchControl</a></td></tr><tr><td class="src">prioCompChoice</td><td class="module"><a href="Agda-Auto-SearchControl.html#v:prioCompChoice">Agda.Auto.SearchControl</a></td></tr><tr><td class="src">prioCompCopy</td><td class="module"><a href="Agda-Auto-SearchControl.html#v:prioCompCopy">Agda.Auto.SearchControl</a></td></tr><tr><td class="src">prioCompIota</td><td class="module"><a href="Agda-Auto-SearchControl.html#v:prioCompIota">Agda.Auto.SearchControl</a></td></tr><tr><td class="src">prioCompUnif</td><td class="module"><a href="Agda-Auto-SearchControl.html#v:prioCompUnif">Agda.Auto.SearchControl</a></td></tr><tr><td class="src">prioInferredTypeUnknown</td><td class="module"><a href="Agda-Auto-SearchControl.html#v:prioInferredTypeUnknown">Agda.Auto.SearchControl</a></td></tr><tr><td class="src">PrioMeta</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Type/Class)</td><td class="module"><a href="Agda-Auto-NarrowingSearch.html#t:PrioMeta">Agda.Auto.NarrowingSearch</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-Auto-NarrowingSearch.html#v:PrioMeta">Agda.Auto.NarrowingSearch</a></td></tr><tr><td class="src">prioNo</td><td class="module"><a href="Agda-Auto-SearchControl.html#v:prioNo">Agda.Auto.SearchControl</a></td></tr><tr><td class="src">prioNoIota</td><td class="module"><a href="Agda-Auto-SearchControl.html#v:prioNoIota">Agda.Auto.SearchControl</a></td></tr><tr><td class="src">prioProjIndex</td><td class="module"><a href="Agda-Auto-SearchControl.html#v:prioProjIndex">Agda.Auto.SearchControl</a></td></tr><tr><td class="src">prioTypecheck</td><td class="module"><a href="Agda-Auto-SearchControl.html#v:prioTypecheck">Agda.Auto.SearchControl</a></td></tr><tr><td class="src">prioTypecheckArgList</td><td class="module"><a href="Agda-Auto-SearchControl.html#v:prioTypecheckArgList">Agda.Auto.SearchControl</a></td></tr><tr><td class="src">prioTypeUnknown</td><td class="module"><a href="Agda-Auto-SearchControl.html#v:prioTypeUnknown">Agda.Auto.SearchControl</a></td></tr><tr><td class="src">Private</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:Private">Agda.Syntax.Concrete</a></td></tr><tr><td class="src">PrivateAccess</td><td class="module"><a href="Agda-Syntax-Common.html#v:PrivateAccess">Agda.Syntax.Common</a></td></tr><tr><td class="src">PrivateNS</td><td class="module"><a href="Agda-Syntax-Scope-Base.html#v:PrivateNS">Agda.Syntax.Scope.Base</a></td></tr><tr><td class="src">prNatEquality</td><td class="module"><a href="Agda-Compiler-Epic-Primitive.html#v:prNatEquality">Agda.Compiler.Epic.Primitive</a></td></tr><tr><td class="src">Problem</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Type/Class)</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Problem.html#t:Problem">Agda.TypeChecking.Rules.LHS.Problem</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Problem.html#v:Problem">Agda.TypeChecking.Rules.LHS.Problem</a></td></tr><tr><td class="src">Problem'</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Problem.html#t:Problem-39-">Agda.TypeChecking.Rules.LHS.Problem</a></td></tr><tr><td class="src">ProblemConstraint</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#t:ProblemConstraint">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">problemFromPats</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-ProblemRest.html#v:problemFromPats">Agda.TypeChecking.Rules.LHS.ProblemRest</a></td></tr><tr><td class="src">ProblemId</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Type/Class)</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#t:ProblemId">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:ProblemId">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">problemInPat</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Problem.html#v:problemInPat">Agda.TypeChecking.Rules.LHS.Problem</a></td></tr><tr><td class="src">problemOutPat</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Problem.html#v:problemOutPat">Agda.TypeChecking.Rules.LHS.Problem</a></td></tr><tr><td class="src">ProblemPart</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Problem.html#t:ProblemPart">Agda.TypeChecking.Rules.LHS.Problem</a></td></tr><tr><td class="src">ProblemRest</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Type/Class)</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Problem.html#t:ProblemRest">Agda.TypeChecking.Rules.LHS.Problem</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Problem.html#v:ProblemRest">Agda.TypeChecking.Rules.LHS.Problem</a></td></tr><tr><td class="src">problemRest</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Problem.html#v:problemRest">Agda.TypeChecking.Rules.LHS.Problem</a></td></tr><tr><td class="src">problemTel</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Problem.html#v:problemTel">Agda.TypeChecking.Rules.LHS.Problem</a></td></tr><tr><td class="src">Proj</td><td class="module"><a href="Agda-Syntax-Internal.html#v:Proj">Agda.Syntax.Internal</a></td></tr><tr><td class="src">ProjectRoot</td><td class="module"><a href="Agda-TypeChecking-Monad-Options.html#v:ProjectRoot">Agda.TypeChecking.Monad.Options</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">projectRoot</td><td class="module"><a href="Agda-Syntax-Concrete-Name.html#v:projectRoot">Agda.Syntax.Concrete.Name</a>, Agda.Syntax.Concrete</td></tr><tr><td class="src">promote</td><td class="module">Agda.Utils.QuickCheck</td></tr><tr><td class="src">proofIrrelevance</td><td class="module"><a href="Agda-TypeChecking-Monad-Options.html#v:proofIrrelevance">Agda.TypeChecking.Monad.Options</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">Prop</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Type/Class)</td><td class="module">Agda.Utils.QuickCheck</td></tr><tr><td class="alt">2 (Type/Class)</td><td class="module"><a href="Agda-Auto-NarrowingSearch.html#t:Prop">Agda.Auto.NarrowingSearch</a></td></tr><tr><td class="alt">3 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:Prop">Agda.Syntax.Concrete</a></td></tr><tr><td class="alt">4 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Internal.html#v:Prop">Agda.Syntax.Internal</a></td></tr><tr><td class="alt">5 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:Prop">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">prop</td><td class="module"><a href="Agda-Syntax-Internal.html#v:prop">Agda.Syntax.Internal</a></td></tr><tr><td class="src">propagatePrio</td><td class="module"><a href="Agda-Auto-NarrowingSearch.html#v:propagatePrio">Agda.Auto.NarrowingSearch</a></td></tr><tr><td class="src">properlyMatching</td><td class="module"><a href="Agda-Syntax-Internal.html#v:properlyMatching">Agda.Syntax.Internal</a></td></tr><tr><td class="src">Property</td><td class="module">Agda.Utils.QuickCheck</td></tr><tr><td class="src">property</td><td class="module">Agda.Utils.QuickCheck</td></tr><tr><td class="src">propFreq</td><td class="module"><a href="Agda-TypeChecking-Test-Generators.html#v:propFreq">Agda.TypeChecking.Test.Generators</a></td></tr><tr><td class="src">PropMustBeSingleton</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:PropMustBeSingleton">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">prop_disjoint</td><td class="module"><a href="Agda-Utils-Warshall.html#v:prop_disjoint">Agda.Utils.Warshall</a></td></tr><tr><td class="src">prop_distinct_fastDistinct</td><td class="module"><a href="Agda-Utils-List.html#v:prop_distinct_fastDistinct">Agda.Utils.List</a></td></tr><tr><td class="src">prop_extractNthElement</td><td class="module"><a href="Agda-Utils-List.html#v:prop_extractNthElement">Agda.Utils.List</a></td></tr><tr><td class="src">prop_flattenTelInv</td><td class="module"><a href="Agda-TypeChecking-Tests.html#v:prop_flattenTelInv">Agda.TypeChecking.Tests</a></td></tr><tr><td class="src">prop_flattenTelScope</td><td class="module"><a href="Agda-TypeChecking-Tests.html#v:prop_flattenTelScope">Agda.TypeChecking.Tests</a></td></tr><tr><td class="src">prop_galois</td><td class="module"><a href="Agda-TypeChecking-Irrelevance.html#v:prop_galois">Agda.TypeChecking.Irrelevance</a></td></tr><tr><td class="src">prop_genericElemIndex</td><td class="module"><a href="Agda-Utils-List.html#v:prop_genericElemIndex">Agda.Utils.List</a></td></tr><tr><td class="src">prop_groupBy'</td><td class="module"><a href="Agda-Utils-List.html#v:prop_groupBy-39-">Agda.Utils.List</a></td></tr><tr><td class="src">prop_path</td><td class="module"><a href="Agda-Utils-Warshall.html#v:prop_path">Agda.Utils.Warshall</a></td></tr><tr><td class="src">prop_reorderTelStable</td><td class="module"><a href="Agda-TypeChecking-Tests.html#v:prop_reorderTelStable">Agda.TypeChecking.Tests</a></td></tr><tr><td class="src">prop_smaller</td><td class="module"><a href="Agda-Utils-Warshall.html#v:prop_smaller">Agda.Utils.Warshall</a></td></tr><tr><td class="src">prop_splitTelescopePermScope</td><td class="module"><a href="Agda-TypeChecking-Tests.html#v:prop_splitTelescopePermScope">Agda.TypeChecking.Tests</a></td></tr><tr><td class="src">prop_splitTelescopeScope</td><td class="module"><a href="Agda-TypeChecking-Tests.html#v:prop_splitTelescopeScope">Agda.TypeChecking.Tests</a></td></tr><tr><td class="src">prop_stable</td><td class="module"><a href="Agda-Utils-Warshall.html#v:prop_stable">Agda.Utils.Warshall</a></td></tr><tr><td class="src">prop_telToListInv</td><td class="module"><a href="Agda-TypeChecking-Tests.html#v:prop_telToListInv">Agda.TypeChecking.Tests</a></td></tr><tr><td class="src">prop_uniqBy</td><td class="module"><a href="Agda-Utils-List.html#v:prop_uniqBy">Agda.Utils.List</a></td></tr><tr><td class="src">prop_wellScopedVars</td><td class="module"><a href="Agda-TypeChecking-Test-Generators.html#v:prop_wellScopedVars">Agda.TypeChecking.Test.Generators</a></td></tr><tr><td class="src">prop_zipWith'</td><td class="module"><a href="Agda-Utils-List.html#v:prop_zipWith-39-">Agda.Utils.List</a></td></tr><tr><td class="src">prPred</td><td class="module"><a href="Agda-Compiler-Epic-Primitive.html#v:prPred">Agda.Compiler.Epic.Primitive</a></td></tr><tr><td class="src">prSuc</td><td class="module"><a href="Agda-Compiler-Epic-Primitive.html#v:prSuc">Agda.Compiler.Epic.Primitive</a></td></tr><tr><td class="src">prTrue</td><td class="module"><a href="Agda-Compiler-Epic-Primitive.html#v:prTrue">Agda.Compiler.Epic.Primitive</a></td></tr><tr><td class="src">prune</td><td class="module"><a href="Agda-TypeChecking-MetaVars-Occurs.html#v:prune">Agda.TypeChecking.MetaVars.Occurs</a></td></tr><tr><td class="src">PrunedEverything</td><td class="module"><a href="Agda-TypeChecking-MetaVars-Occurs.html#v:PrunedEverything">Agda.TypeChecking.MetaVars.Occurs</a></td></tr><tr><td class="src">PrunedNothing</td><td class="module"><a href="Agda-TypeChecking-MetaVars-Occurs.html#v:PrunedNothing">Agda.TypeChecking.MetaVars.Occurs</a></td></tr><tr><td class="src">PrunedSomething</td><td class="module"><a href="Agda-TypeChecking-MetaVars-Occurs.html#v:PrunedSomething">Agda.TypeChecking.MetaVars.Occurs</a></td></tr><tr><td class="src">PruneResult</td><td class="module"><a href="Agda-TypeChecking-MetaVars-Occurs.html#t:PruneResult">Agda.TypeChecking.MetaVars.Occurs</a></td></tr><tr><td class="src">prZero</td><td class="module"><a href="Agda-Compiler-Epic-Primitive.html#v:prZero">Agda.Compiler.Epic.Primitive</a></td></tr><tr><td class="src">PState</td><td class="module"><a href="Agda-Syntax-Parser-Monad.html#v:PState">Agda.Syntax.Parser.Monad</a></td></tr><tr><td class="src">PStr</td><td class="module">Agda.Utils.Pretty</td></tr><tr><td class="src">ptext</td><td class="module">Agda.Utils.Pretty</td></tr><tr><td class="src">Ptr</td><td class="module"><a href="Agda-Utils-Pointer.html#t:Ptr">Agda.Utils.Pointer</a>, Agda.Syntax.Internal</td></tr><tr><td class="src">PublicAccess</td><td class="module"><a href="Agda-Syntax-Common.html#v:PublicAccess">Agda.Syntax.Common</a></td></tr><tr><td class="src">publicModules</td><td class="module"><a href="Agda-Syntax-Scope-Base.html#v:publicModules">Agda.Syntax.Scope.Base</a></td></tr><tr><td class="src">PublicNS</td><td class="module"><a href="Agda-Syntax-Scope-Base.html#v:PublicNS">Agda.Syntax.Scope.Base</a></td></tr><tr><td class="src">publicOpen</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:publicOpen">Agda.Syntax.Concrete</a></td></tr><tr><td class="src">punct</td><td class="module"><a href="Agda-Compiler-JS-Parser.html#v:punct">Agda.Compiler.JS.Parser</a></td></tr><tr><td class="src">punctuate</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Function)</td><td class="module">Agda.Utils.Pretty</td></tr><tr><td class="alt">2 (Function)</td><td class="module"><a href="Agda-TypeChecking-Pretty.html#v:punctuate">Agda.TypeChecking.Pretty</a></td></tr><tr><td class="src">pureTCM</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:pureTCM">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">purgeNonvariant</td><td class="module"><a href="Agda-TypeChecking-Polarity.html#v:purgeNonvariant">Agda.TypeChecking.Polarity</a></td></tr><tr><td class="src">pushContext</td><td class="module"><a href="Agda-Syntax-Parser-Monad.html#v:pushContext">Agda.Syntax.Parser.Monad</a></td></tr><tr><td class="src">pushCurrentContext</td><td class="module"><a href="Agda-Syntax-Parser-Monad.html#v:pushCurrentContext">Agda.Syntax.Parser.Monad</a></td></tr><tr><td class="src">pushLexState</td><td class="module"><a href="Agda-Syntax-Parser-Monad.html#v:pushLexState">Agda.Syntax.Parser.Monad</a></td></tr><tr><td class="src">putAllConstraintsToSleep</td><td class="module"><a href="Agda-TypeChecking-Monad-Constraints.html#v:putAllConstraintsToSleep">Agda.TypeChecking.Monad.Constraints</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">putConArity</td><td class="module"><a href="Agda-Compiler-Epic-CompileState.html#v:putConArity">Agda.Compiler.Epic.CompileState</a></td></tr><tr><td class="src">putConstrTag</td><td class="module"><a href="Agda-Compiler-Epic-CompileState.html#v:putConstrTag">Agda.Compiler.Epic.CompileState</a></td></tr><tr><td class="src">putDelayed</td><td class="module"><a href="Agda-Compiler-Epic-CompileState.html#v:putDelayed">Agda.Compiler.Epic.CompileState</a></td></tr><tr><td class="src">putForcedArgs</td><td class="module"><a href="Agda-Compiler-Epic-CompileState.html#v:putForcedArgs">Agda.Compiler.Epic.CompileState</a></td></tr><tr><td class="src">putMain</td><td class="module"><a href="Agda-Compiler-Epic-CompileState.html#v:putMain">Agda.Compiler.Epic.CompileState</a></td></tr><tr><td class="src">putResponse</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Function)</td><td class="module"><a href="Agda-Interaction-EmacsCommand.html#v:putResponse">Agda.Interaction.EmacsCommand</a></td></tr><tr><td class="alt">2 (Function)</td><td class="module"><a href="Agda-Interaction-InteractionTop.html#v:putResponse">Agda.Interaction.InteractionTop</a></td></tr><tr><td class="src">pwords</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Function)</td><td class="module"><a href="Agda-Utils-Pretty.html#v:pwords">Agda.Utils.Pretty</a></td></tr><tr><td class="alt">2 (Function)</td><td class="module"><a href="Agda-TypeChecking-Pretty.html#v:pwords">Agda.TypeChecking.Pretty</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>