<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"><html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>Agda.TypeChecking.Primitive</title><link href="ocean.css" rel="stylesheet" type="text/css" title="Ocean" /><script src="haddock-util.js" type="text/javascript"></script><script type="text/javascript">//<![CDATA[
window.onload = function () {pageLoad();setSynopsis("mini_Agda-TypeChecking-Primitive.html");};
//]]>
</script></head><body><div id="package-header"><ul class="links" id="page-menu"><li><a href="src/Agda-TypeChecking-Primitive.html">Source</a></li><li><a href="index.html">Contents</a></li><li><a href="doc-index.html">Index</a></li></ul><p class="caption">Agda-2.3.2.1: A dependently typed functional programming language and proof assistant</p></div><div id="content"><div id="module-header"><table class="info"><tr><th>Safe Haskell</th><td>None</td></tr></table><p class="caption">Agda.TypeChecking.Primitive</p></div><div id="table-of-contents"><p class="caption">Contents</p><ul><li><a href="#g:1">Primitive functions
</a></li><li><a href="#g:2">The actual primitive functions
</a></li></ul></div><div id="description"><p class="caption">Description</p><div class="doc"><p>Primitive functions, such as addition on builtin integers.
</p></div></div><div id="synopsis"><p id="control.syn" class="caption expander" onclick="toggleSection('syn')">Synopsis</p><ul id="section.syn" class="hide" onclick="toggleSection('syn')"><li class="src short"><a href="#v:constructorForm">constructorForm</a> :: <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a></li><li class="src short"><span class="keyword">data</span> <a href="#t:PrimitiveImpl">PrimitiveImpl</a> = <a href="#v:PrimImpl">PrimImpl</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> <a href="Agda-TypeChecking-Monad-Base.html#t:PrimFun">PrimFun</a></li><li class="src short"><span class="keyword">newtype</span> <a href="#t:Str">Str</a> = <a href="#v:Str">Str</a> {<ul class="subs"><li><a href="#v:unStr">unStr</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a></li></ul>}</li><li class="src short"><span class="keyword">newtype</span> <a href="#t:Nat">Nat</a> = <a href="#v:Nat">Nat</a> {<ul class="subs"><li><a href="#v:unNat">unNat</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Prelude.html#t:Integer">Integer</a></li></ul>}</li><li class="src short"><span class="keyword">newtype</span> <a href="#t:Lvl">Lvl</a> = <a href="#v:Lvl">Lvl</a> {<ul class="subs"><li><a href="#v:unLvl">unLvl</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Prelude.html#t:Integer">Integer</a></li></ul>}</li><li class="src short"><span class="keyword">class</span> <a href="#t:PrimType">PrimType</a> a <span class="keyword">where</span><ul class="subs"><li><a href="#v:primType">primType</a> :: a -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a></li></ul></li><li class="src short"><span class="keyword">class</span> <a href="#t:PrimTerm">PrimTerm</a> a <span class="keyword">where</span><ul class="subs"><li><a href="#v:primTerm">primTerm</a> :: a -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a></li></ul></li><li class="src short"><span class="keyword">class</span> <a href="#t:ToTerm">ToTerm</a> a <span class="keyword">where</span><ul class="subs"><li><a href="#v:toTerm">toTerm</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> (a -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a>)</li></ul></li><li class="src short"><a href="#v:buildList">buildList</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> ([<a href="Agda-Syntax-Internal.html#t:Term">Term</a>] -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a>)</li><li class="src short"><span class="keyword">type</span> <a href="#t:FromTermFunction">FromTermFunction</a> a = <a href="Agda-Syntax-Common.html#t:Arg">Arg</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> (<a href="Agda-TypeChecking-Monad-Base.html#t:Reduced">Reduced</a> (<a href="Agda-TypeChecking-Monad-Base.html#t:MaybeReduced">MaybeReduced</a> (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a>)) a)</li><li class="src short"><span class="keyword">class</span> <a href="#t:FromTerm">FromTerm</a> a <span class="keyword">where</span><ul class="subs"><li><a href="#v:fromTerm">fromTerm</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> (<a href="Agda-TypeChecking-Primitive.html#t:FromTermFunction">FromTermFunction</a> a)</li></ul></li><li class="src short"><a href="#v:redBind">redBind</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> (<a href="Agda-TypeChecking-Monad-Base.html#t:Reduced">Reduced</a> a a') -> (a -> b) -> (a' -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> (<a href="Agda-TypeChecking-Monad-Base.html#t:Reduced">Reduced</a> b b')) -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> (<a href="Agda-TypeChecking-Monad-Base.html#t:Reduced">Reduced</a> b b')</li><li class="src short"><a href="#v:redReturn">redReturn</a> :: a -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> (<a href="Agda-TypeChecking-Monad-Base.html#t:Reduced">Reduced</a> a' a)</li><li class="src short"><a href="#v:fromReducedTerm">fromReducedTerm</a> :: (<a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> a) -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> (<a href="Agda-TypeChecking-Primitive.html#t:FromTermFunction">FromTermFunction</a> a)</li><li class="src short"><a href="#v:fromLiteral">fromLiteral</a> :: (<a href="Agda-Syntax-Literal.html#t:Literal">Literal</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> a) -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> (<a href="Agda-TypeChecking-Primitive.html#t:FromTermFunction">FromTermFunction</a> a)</li><li class="src short"><a href="#v:primTrustMe">primTrustMe</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-Primitive.html#t:PrimitiveImpl">PrimitiveImpl</a></li><li class="src short"><a href="#v:primQNameType">primQNameType</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-Primitive.html#t:PrimitiveImpl">PrimitiveImpl</a></li><li class="src short"><a href="#v:primQNameDefinition">primQNameDefinition</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-Primitive.html#t:PrimitiveImpl">PrimitiveImpl</a></li><li class="src short"><a href="#v:primDataConstructors">primDataConstructors</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-Primitive.html#t:PrimitiveImpl">PrimitiveImpl</a></li><li class="src short"><a href="#v:mkPrimLevelZero">mkPrimLevelZero</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-Primitive.html#t:PrimitiveImpl">PrimitiveImpl</a></li><li class="src short"><a href="#v:mkPrimLevelSuc">mkPrimLevelSuc</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-Primitive.html#t:PrimitiveImpl">PrimitiveImpl</a></li><li class="src short"><a href="#v:mkPrimLevelMax">mkPrimLevelMax</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-Primitive.html#t:PrimitiveImpl">PrimitiveImpl</a></li><li class="src short"><a href="#v:mkPrimFun1TCM">mkPrimFun1TCM</a> :: (<a href="Agda-TypeChecking-Primitive.html#t:FromTerm">FromTerm</a> a, <a href="Agda-TypeChecking-Primitive.html#t:ToTerm">ToTerm</a> b) => <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> (a -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> b) -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-Primitive.html#t:PrimitiveImpl">PrimitiveImpl</a></li><li class="src short"><a href="#v:mkPrimFun1">mkPrimFun1</a> :: (<a href="Agda-TypeChecking-Primitive.html#t:PrimType">PrimType</a> a, <a href="Agda-TypeChecking-Primitive.html#t:PrimType">PrimType</a> b, <a href="Agda-TypeChecking-Primitive.html#t:FromTerm">FromTerm</a> a, <a href="Agda-TypeChecking-Primitive.html#t:ToTerm">ToTerm</a> b) => (a -> b) -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-Primitive.html#t:PrimitiveImpl">PrimitiveImpl</a></li><li class="src short"><a href="#v:mkPrimFun2">mkPrimFun2</a> :: (<a href="Agda-TypeChecking-Primitive.html#t:PrimType">PrimType</a> a, <a href="Agda-TypeChecking-Primitive.html#t:PrimType">PrimType</a> b, <a href="Agda-TypeChecking-Primitive.html#t:PrimType">PrimType</a> c, <a href="Agda-TypeChecking-Primitive.html#t:FromTerm">FromTerm</a> a, <a href="Agda-TypeChecking-Primitive.html#t:ToTerm">ToTerm</a> a, <a href="Agda-TypeChecking-Primitive.html#t:FromTerm">FromTerm</a> b, <a href="Agda-TypeChecking-Primitive.html#t:ToTerm">ToTerm</a> c) => (a -> b -> c) -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-Primitive.html#t:PrimitiveImpl">PrimitiveImpl</a></li><li class="src short"><a href="#v:mkPrimFun4">mkPrimFun4</a> :: (<a href="Agda-TypeChecking-Primitive.html#t:PrimType">PrimType</a> a, <a href="Agda-TypeChecking-Primitive.html#t:FromTerm">FromTerm</a> a, <a href="Agda-TypeChecking-Primitive.html#t:ToTerm">ToTerm</a> a, <a href="Agda-TypeChecking-Primitive.html#t:PrimType">PrimType</a> b, <a href="Agda-TypeChecking-Primitive.html#t:FromTerm">FromTerm</a> b, <a href="Agda-TypeChecking-Primitive.html#t:ToTerm">ToTerm</a> b, <a href="Agda-TypeChecking-Primitive.html#t:PrimType">PrimType</a> c, <a href="Agda-TypeChecking-Primitive.html#t:FromTerm">FromTerm</a> c, <a href="Agda-TypeChecking-Primitive.html#t:ToTerm">ToTerm</a> c, <a href="Agda-TypeChecking-Primitive.html#t:PrimType">PrimType</a> d, <a href="Agda-TypeChecking-Primitive.html#t:FromTerm">FromTerm</a> d, <a href="Agda-TypeChecking-Primitive.html#t:PrimType">PrimType</a> e, <a href="Agda-TypeChecking-Primitive.html#t:ToTerm">ToTerm</a> e) => (a -> b -> c -> d -> e) -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-Primitive.html#t:PrimitiveImpl">PrimitiveImpl</a></li><li class="src short"><a href="#v:-45--45--62-">(-->)</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a></li><li class="src short"><a href="#v:.-45--45--62-">(.-->)</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a></li><li class="src short"><a href="#v:gpi">gpi</a> :: <a href="Agda-Syntax-Common.html#t:Hiding">Hiding</a> -> <a href="Agda-Syntax-Common.html#t:Relevance">Relevance</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a></li><li class="src short"><a href="#v:hPi">hPi</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a></li><li class="src short"><a href="#v:nPi">nPi</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a></li><li class="src short"><a href="#v:varM">varM</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a></li><li class="src short"><a href="#v:gApply">gApply</a> :: <a href="Agda-Syntax-Common.html#t:Hiding">Hiding</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a></li><li class="src short"><a href="#v:-60--64--62-">(<@>)</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a></li><li class="src short"><a href="#v:-60--35--62-">(<#>)</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a></li><li class="src short"><a href="#v:list">list</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a></li><li class="src short"><a href="#v:io">io</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a></li><li class="src short"><a href="#v:el">el</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a></li><li class="src short"><a href="#v:tset">tset</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a></li><li class="src short"><a href="#v:argN">argN</a> :: e -> <a href="Agda-Syntax-Common.html#t:Arg">Arg</a> e</li><li class="src short"><a href="#v:domN">domN</a> :: e -> <a href="Agda-Syntax-Common.html#t:Dom">Dom</a> e</li><li class="src short"><a href="#v:argH">argH</a> :: e -> <a href="Agda-Syntax-Common.html#t:Arg">Arg</a> e</li><li class="src short"><a href="#v:domH">domH</a> :: e -> <a href="Agda-Syntax-Common.html#t:Dom">Dom</a> e</li><li class="src short"><span class="keyword">type</span> <a href="#t:Op">Op</a> a = a -> a -> a</li><li class="src short"><span class="keyword">type</span> <a href="#t:Fun">Fun</a> a = a -> a</li><li class="src short"><span class="keyword">type</span> <a href="#t:Rel">Rel</a> a = a -> a -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li class="src short"><span class="keyword">type</span> <a href="#t:Pred">Pred</a> a = a -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li class="src short"><a href="#v:primitiveFunctions">primitiveFunctions</a> :: <a href="/usr/share/doc/ghc/html/libraries/containers-0.4.2.1/Data-Map.html#t:Map">Map</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> (<a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-Primitive.html#t:PrimitiveImpl">PrimitiveImpl</a>)</li><li class="src short"><a href="#v:lookupPrimitiveFunction">lookupPrimitiveFunction</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-Primitive.html#t:PrimitiveImpl">PrimitiveImpl</a></li><li class="src short"><a href="#v:lookupPrimitiveFunctionQ">lookupPrimitiveFunctionQ</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a>, <a href="Agda-TypeChecking-Primitive.html#t:PrimitiveImpl">PrimitiveImpl</a>)</li></ul></div><div id="interface"><h1>Documentation</h1><div class="top"><p class="src"><a name="v:constructorForm" class="def">constructorForm</a> :: <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a><a href="src/Agda-TypeChecking-Primitive.html#constructorForm" class="link">Source</a></p><div class="doc"><p>Rewrite a literal to constructor form if possible.
</p></div></div><h1 id="g:1">Primitive functions
</h1><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:PrimitiveImpl" class="def">PrimitiveImpl</a> <a href="src/Agda-TypeChecking-Primitive.html#PrimitiveImpl" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:PrimImpl" class="def">PrimImpl</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> <a href="Agda-TypeChecking-Monad-Base.html#t:PrimFun">PrimFun</a></td><td class="doc empty"> </td></tr></table></div></div><div class="top"><p class="src"><span class="keyword">newtype</span> <a name="t:Str" class="def">Str</a> <a href="src/Agda-TypeChecking-Primitive.html#Str" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:Str" class="def">Str</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div class="subs fields"><p class="caption">Fields</p><dl><dt class="src"><a name="v:unStr" class="def">unStr</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a></dt><dd class="doc empty"> </dd></dl><div class="clear"></div></div></td></tr></table></div><div class="subs instances"><p id="control.i:Str" class="caption collapser" onclick="toggleSection('i:Str')">Instances</p><div id="section.i:Str" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Eq.html#t:Eq">Eq</a> <a href="Agda-TypeChecking-Primitive.html#t:Str">Str</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Ord.html#t:Ord">Ord</a> <a href="Agda-TypeChecking-Primitive.html#t:Str">Str</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Primitive.html#t:FromTerm">FromTerm</a> <a href="Agda-TypeChecking-Primitive.html#t:Str">Str</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Primitive.html#t:ToTerm">ToTerm</a> <a href="Agda-TypeChecking-Primitive.html#t:Str">Str</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Primitive.html#t:PrimTerm">PrimTerm</a> <a href="Agda-TypeChecking-Primitive.html#t:Str">Str</a></td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><span class="keyword">newtype</span> <a name="t:Nat" class="def">Nat</a> <a href="src/Agda-TypeChecking-Primitive.html#Nat" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:Nat" class="def">Nat</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div class="subs fields"><p class="caption">Fields</p><dl><dt class="src"><a name="v:unNat" class="def">unNat</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Prelude.html#t:Integer">Integer</a></dt><dd class="doc empty"> </dd></dl><div class="clear"></div></div></td></tr></table></div><div class="subs instances"><p id="control.i:Nat" class="caption collapser" onclick="toggleSection('i:Nat')">Instances</p><div id="section.i:Nat" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Prelude.html#t:Enum">Enum</a> <a href="Agda-TypeChecking-Primitive.html#t:Nat">Nat</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Eq.html#t:Eq">Eq</a> <a href="Agda-TypeChecking-Primitive.html#t:Nat">Nat</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Prelude.html#t:Integral">Integral</a> <a href="Agda-TypeChecking-Primitive.html#t:Nat">Nat</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Prelude.html#t:Num">Num</a> <a href="Agda-TypeChecking-Primitive.html#t:Nat">Nat</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Ord.html#t:Ord">Ord</a> <a href="Agda-TypeChecking-Primitive.html#t:Nat">Nat</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Prelude.html#t:Real">Real</a> <a href="Agda-TypeChecking-Primitive.html#t:Nat">Nat</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Text-Show.html#t:Show">Show</a> <a href="Agda-TypeChecking-Primitive.html#t:Nat">Nat</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Primitive.html#t:FromTerm">FromTerm</a> <a href="Agda-TypeChecking-Primitive.html#t:Nat">Nat</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Primitive.html#t:ToTerm">ToTerm</a> <a href="Agda-TypeChecking-Primitive.html#t:Nat">Nat</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Primitive.html#t:PrimTerm">PrimTerm</a> <a href="Agda-TypeChecking-Primitive.html#t:Nat">Nat</a></td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><span class="keyword">newtype</span> <a name="t:Lvl" class="def">Lvl</a> <a href="src/Agda-TypeChecking-Primitive.html#Lvl" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:Lvl" class="def">Lvl</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div class="subs fields"><p class="caption">Fields</p><dl><dt class="src"><a name="v:unLvl" class="def">unLvl</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Prelude.html#t:Integer">Integer</a></dt><dd class="doc empty"> </dd></dl><div class="clear"></div></div></td></tr></table></div><div class="subs instances"><p id="control.i:Lvl" class="caption collapser" onclick="toggleSection('i:Lvl')">Instances</p><div id="section.i:Lvl" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Eq.html#t:Eq">Eq</a> <a href="Agda-TypeChecking-Primitive.html#t:Lvl">Lvl</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Ord.html#t:Ord">Ord</a> <a href="Agda-TypeChecking-Primitive.html#t:Lvl">Lvl</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Text-Show.html#t:Show">Show</a> <a href="Agda-TypeChecking-Primitive.html#t:Lvl">Lvl</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Primitive.html#t:FromTerm">FromTerm</a> <a href="Agda-TypeChecking-Primitive.html#t:Lvl">Lvl</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Primitive.html#t:ToTerm">ToTerm</a> <a href="Agda-TypeChecking-Primitive.html#t:Lvl">Lvl</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Primitive.html#t:PrimTerm">PrimTerm</a> <a href="Agda-TypeChecking-Primitive.html#t:Lvl">Lvl</a></td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><span class="keyword">class</span> <a name="t:PrimType" class="def">PrimType</a> a <span class="keyword">where</span><a href="src/Agda-TypeChecking-Primitive.html#PrimType" class="link">Source</a></p><div class="subs methods"><p class="caption">Methods</p><p class="src"><a name="v:primType" class="def">primType</a> :: a -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a><a href="src/Agda-TypeChecking-Primitive.html#primType" class="link">Source</a></p></div><div class="subs instances"><p id="control.i:PrimType" class="caption collapser" onclick="toggleSection('i:PrimType')">Instances</p><div id="section.i:PrimType" class="show"><table><tr><td class="src"><a href="Agda-TypeChecking-Primitive.html#t:PrimTerm">PrimTerm</a> a => <a href="Agda-TypeChecking-Primitive.html#t:PrimType">PrimType</a> a</td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><span class="keyword">class</span> <a name="t:PrimTerm" class="def">PrimTerm</a> a <span class="keyword">where</span><a href="src/Agda-TypeChecking-Primitive.html#PrimTerm" class="link">Source</a></p><div class="subs methods"><p class="caption">Methods</p><p class="src"><a name="v:primTerm" class="def">primTerm</a> :: a -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a><a href="src/Agda-TypeChecking-Primitive.html#primTerm" class="link">Source</a></p></div><div class="subs instances"><p id="control.i:PrimTerm" class="caption collapser" onclick="toggleSection('i:PrimTerm')">Instances</p><div id="section.i:PrimTerm" class="show"><table><tr><td class="src"><a href="Agda-TypeChecking-Primitive.html#t:PrimTerm">PrimTerm</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Primitive.html#t:PrimTerm">PrimTerm</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Char.html#t:Char">Char</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Primitive.html#t:PrimTerm">PrimTerm</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Prelude.html#t:Double">Double</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Primitive.html#t:PrimTerm">PrimTerm</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Prelude.html#t:Integer">Integer</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Primitive.html#t:PrimTerm">PrimTerm</a> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Primitive.html#t:PrimTerm">PrimTerm</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Primitive.html#t:PrimTerm">PrimTerm</a> <a href="Agda-TypeChecking-Primitive.html#t:Lvl">Lvl</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Primitive.html#t:PrimTerm">PrimTerm</a> <a href="Agda-TypeChecking-Primitive.html#t:Nat">Nat</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Primitive.html#t:PrimTerm">PrimTerm</a> <a href="Agda-TypeChecking-Primitive.html#t:Str">Str</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Primitive.html#t:PrimTerm">PrimTerm</a> a => <a href="Agda-TypeChecking-Primitive.html#t:PrimTerm">PrimTerm</a> [a]</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Primitive.html#t:PrimTerm">PrimTerm</a> a => <a href="Agda-TypeChecking-Primitive.html#t:PrimTerm">PrimTerm</a> (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:IO">IO</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src">(<a href="Agda-TypeChecking-Primitive.html#t:PrimType">PrimType</a> a, <a href="Agda-TypeChecking-Primitive.html#t:PrimType">PrimType</a> b) => <a href="Agda-TypeChecking-Primitive.html#t:PrimTerm">PrimTerm</a> (a -> b)</td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><span class="keyword">class</span> <a name="t:ToTerm" class="def">ToTerm</a> a <span class="keyword">where</span><a href="src/Agda-TypeChecking-Primitive.html#ToTerm" class="link">Source</a></p><div class="subs methods"><p class="caption">Methods</p><p class="src"><a name="v:toTerm" class="def">toTerm</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> (a -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a>)<a href="src/Agda-TypeChecking-Primitive.html#toTerm" class="link">Source</a></p></div><div class="subs instances"><p id="control.i:ToTerm" class="caption collapser" onclick="toggleSection('i:ToTerm')">Instances</p><div id="section.i:ToTerm" class="show"><table><tr><td class="src"><a href="Agda-TypeChecking-Primitive.html#t:ToTerm">ToTerm</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Primitive.html#t:ToTerm">ToTerm</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Char.html#t:Char">Char</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Primitive.html#t:ToTerm">ToTerm</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Prelude.html#t:Double">Double</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Primitive.html#t:ToTerm">ToTerm</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Prelude.html#t:Integer">Integer</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Primitive.html#t:ToTerm">ToTerm</a> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Primitive.html#t:ToTerm">ToTerm</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Primitive.html#t:ToTerm">ToTerm</a> <a href="Agda-TypeChecking-Primitive.html#t:Lvl">Lvl</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Primitive.html#t:ToTerm">ToTerm</a> <a href="Agda-TypeChecking-Primitive.html#t:Nat">Nat</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Primitive.html#t:ToTerm">ToTerm</a> <a href="Agda-TypeChecking-Primitive.html#t:Str">Str</a></td><td class="doc empty"> </td></tr><tr><td class="src">(<a href="Agda-TypeChecking-Primitive.html#t:PrimTerm">PrimTerm</a> a, <a href="Agda-TypeChecking-Primitive.html#t:ToTerm">ToTerm</a> a) => <a href="Agda-TypeChecking-Primitive.html#t:ToTerm">ToTerm</a> [a]</td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><a name="v:buildList" class="def">buildList</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> ([<a href="Agda-Syntax-Internal.html#t:Term">Term</a>] -> <a href="Agda-Syntax-Internal.html#t:Term">Term</a>)<a href="src/Agda-TypeChecking-Primitive.html#buildList" class="link">Source</a></p><div class="doc"><p><code>buildList A ts</code> builds a list of type <code>List A</code>. Assumes that the terms
<code>ts</code> all have type <code>A</code>.
</p></div></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:FromTermFunction" class="def">FromTermFunction</a> a = <a href="Agda-Syntax-Common.html#t:Arg">Arg</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> (<a href="Agda-TypeChecking-Monad-Base.html#t:Reduced">Reduced</a> (<a href="Agda-TypeChecking-Monad-Base.html#t:MaybeReduced">MaybeReduced</a> (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a>)) a)<a href="src/Agda-TypeChecking-Primitive.html#FromTermFunction" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">class</span> <a name="t:FromTerm" class="def">FromTerm</a> a <span class="keyword">where</span><a href="src/Agda-TypeChecking-Primitive.html#FromTerm" class="link">Source</a></p><div class="subs methods"><p class="caption">Methods</p><p class="src"><a name="v:fromTerm" class="def">fromTerm</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> (<a href="Agda-TypeChecking-Primitive.html#t:FromTermFunction">FromTermFunction</a> a)<a href="src/Agda-TypeChecking-Primitive.html#fromTerm" class="link">Source</a></p></div><div class="subs instances"><p id="control.i:FromTerm" class="caption collapser" onclick="toggleSection('i:FromTerm')">Instances</p><div id="section.i:FromTerm" class="show"><table><tr><td class="src"><a href="Agda-TypeChecking-Primitive.html#t:FromTerm">FromTerm</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Primitive.html#t:FromTerm">FromTerm</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Char.html#t:Char">Char</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Primitive.html#t:FromTerm">FromTerm</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Prelude.html#t:Double">Double</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Primitive.html#t:FromTerm">FromTerm</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Prelude.html#t:Integer">Integer</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Primitive.html#t:FromTerm">FromTerm</a> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Primitive.html#t:FromTerm">FromTerm</a> <a href="Agda-TypeChecking-Primitive.html#t:Lvl">Lvl</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Primitive.html#t:FromTerm">FromTerm</a> <a href="Agda-TypeChecking-Primitive.html#t:Nat">Nat</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Primitive.html#t:FromTerm">FromTerm</a> <a href="Agda-TypeChecking-Primitive.html#t:Str">Str</a></td><td class="doc empty"> </td></tr><tr><td class="src">(<a href="Agda-TypeChecking-Primitive.html#t:ToTerm">ToTerm</a> a, <a href="Agda-TypeChecking-Primitive.html#t:FromTerm">FromTerm</a> a) => <a href="Agda-TypeChecking-Primitive.html#t:FromTerm">FromTerm</a> [a]</td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><a name="v:redBind" class="def">redBind</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> (<a href="Agda-TypeChecking-Monad-Base.html#t:Reduced">Reduced</a> a a') -> (a -> b) -> (a' -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> (<a href="Agda-TypeChecking-Monad-Base.html#t:Reduced">Reduced</a> b b')) -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> (<a href="Agda-TypeChecking-Monad-Base.html#t:Reduced">Reduced</a> b b')<a href="src/Agda-TypeChecking-Primitive.html#redBind" class="link">Source</a></p><div class="doc"><p>Conceptually: <code>redBind m f k = either (return . Left . f) k =<< m</code>
</p></div></div><div class="top"><p class="src"><a name="v:redReturn" class="def">redReturn</a> :: a -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> (<a href="Agda-TypeChecking-Monad-Base.html#t:Reduced">Reduced</a> a' a)<a href="src/Agda-TypeChecking-Primitive.html#redReturn" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:fromReducedTerm" class="def">fromReducedTerm</a> :: (<a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> a) -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> (<a href="Agda-TypeChecking-Primitive.html#t:FromTermFunction">FromTermFunction</a> a)<a href="src/Agda-TypeChecking-Primitive.html#fromReducedTerm" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:fromLiteral" class="def">fromLiteral</a> :: (<a href="Agda-Syntax-Literal.html#t:Literal">Literal</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> a) -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> (<a href="Agda-TypeChecking-Primitive.html#t:FromTermFunction">FromTermFunction</a> a)<a href="src/Agda-TypeChecking-Primitive.html#fromLiteral" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:primTrustMe" class="def">primTrustMe</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-Primitive.html#t:PrimitiveImpl">PrimitiveImpl</a><a href="src/Agda-TypeChecking-Primitive.html#primTrustMe" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:primQNameType" class="def">primQNameType</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-Primitive.html#t:PrimitiveImpl">PrimitiveImpl</a><a href="src/Agda-TypeChecking-Primitive.html#primQNameType" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:primQNameDefinition" class="def">primQNameDefinition</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-Primitive.html#t:PrimitiveImpl">PrimitiveImpl</a><a href="src/Agda-TypeChecking-Primitive.html#primQNameDefinition" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:primDataConstructors" class="def">primDataConstructors</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-Primitive.html#t:PrimitiveImpl">PrimitiveImpl</a><a href="src/Agda-TypeChecking-Primitive.html#primDataConstructors" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:mkPrimLevelZero" class="def">mkPrimLevelZero</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-Primitive.html#t:PrimitiveImpl">PrimitiveImpl</a><a href="src/Agda-TypeChecking-Primitive.html#mkPrimLevelZero" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:mkPrimLevelSuc" class="def">mkPrimLevelSuc</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-Primitive.html#t:PrimitiveImpl">PrimitiveImpl</a><a href="src/Agda-TypeChecking-Primitive.html#mkPrimLevelSuc" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:mkPrimLevelMax" class="def">mkPrimLevelMax</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-Primitive.html#t:PrimitiveImpl">PrimitiveImpl</a><a href="src/Agda-TypeChecking-Primitive.html#mkPrimLevelMax" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:mkPrimFun1TCM" class="def">mkPrimFun1TCM</a> :: (<a href="Agda-TypeChecking-Primitive.html#t:FromTerm">FromTerm</a> a, <a href="Agda-TypeChecking-Primitive.html#t:ToTerm">ToTerm</a> b) => <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> (a -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> b) -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-Primitive.html#t:PrimitiveImpl">PrimitiveImpl</a><a href="src/Agda-TypeChecking-Primitive.html#mkPrimFun1TCM" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:mkPrimFun1" class="def">mkPrimFun1</a> :: (<a href="Agda-TypeChecking-Primitive.html#t:PrimType">PrimType</a> a, <a href="Agda-TypeChecking-Primitive.html#t:PrimType">PrimType</a> b, <a href="Agda-TypeChecking-Primitive.html#t:FromTerm">FromTerm</a> a, <a href="Agda-TypeChecking-Primitive.html#t:ToTerm">ToTerm</a> b) => (a -> b) -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-Primitive.html#t:PrimitiveImpl">PrimitiveImpl</a><a href="src/Agda-TypeChecking-Primitive.html#mkPrimFun1" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:mkPrimFun2" class="def">mkPrimFun2</a> :: (<a href="Agda-TypeChecking-Primitive.html#t:PrimType">PrimType</a> a, <a href="Agda-TypeChecking-Primitive.html#t:PrimType">PrimType</a> b, <a href="Agda-TypeChecking-Primitive.html#t:PrimType">PrimType</a> c, <a href="Agda-TypeChecking-Primitive.html#t:FromTerm">FromTerm</a> a, <a href="Agda-TypeChecking-Primitive.html#t:ToTerm">ToTerm</a> a, <a href="Agda-TypeChecking-Primitive.html#t:FromTerm">FromTerm</a> b, <a href="Agda-TypeChecking-Primitive.html#t:ToTerm">ToTerm</a> c) => (a -> b -> c) -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-Primitive.html#t:PrimitiveImpl">PrimitiveImpl</a><a href="src/Agda-TypeChecking-Primitive.html#mkPrimFun2" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:mkPrimFun4" class="def">mkPrimFun4</a> :: (<a href="Agda-TypeChecking-Primitive.html#t:PrimType">PrimType</a> a, <a href="Agda-TypeChecking-Primitive.html#t:FromTerm">FromTerm</a> a, <a href="Agda-TypeChecking-Primitive.html#t:ToTerm">ToTerm</a> a, <a href="Agda-TypeChecking-Primitive.html#t:PrimType">PrimType</a> b, <a href="Agda-TypeChecking-Primitive.html#t:FromTerm">FromTerm</a> b, <a href="Agda-TypeChecking-Primitive.html#t:ToTerm">ToTerm</a> b, <a href="Agda-TypeChecking-Primitive.html#t:PrimType">PrimType</a> c, <a href="Agda-TypeChecking-Primitive.html#t:FromTerm">FromTerm</a> c, <a href="Agda-TypeChecking-Primitive.html#t:ToTerm">ToTerm</a> c, <a href="Agda-TypeChecking-Primitive.html#t:PrimType">PrimType</a> d, <a href="Agda-TypeChecking-Primitive.html#t:FromTerm">FromTerm</a> d, <a href="Agda-TypeChecking-Primitive.html#t:PrimType">PrimType</a> e, <a href="Agda-TypeChecking-Primitive.html#t:ToTerm">ToTerm</a> e) => (a -> b -> c -> d -> e) -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-Primitive.html#t:PrimitiveImpl">PrimitiveImpl</a><a href="src/Agda-TypeChecking-Primitive.html#mkPrimFun4" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:-45--45--62-" class="def">(-->)</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a><a href="src/Agda-TypeChecking-Primitive.html#--%3E" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:.-45--45--62-" class="def">(.-->)</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a><a href="src/Agda-TypeChecking-Primitive.html#.--%3E" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:gpi" class="def">gpi</a> :: <a href="Agda-Syntax-Common.html#t:Hiding">Hiding</a> -> <a href="Agda-Syntax-Common.html#t:Relevance">Relevance</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a><a href="src/Agda-TypeChecking-Primitive.html#gpi" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:hPi" class="def">hPi</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a><a href="src/Agda-TypeChecking-Primitive.html#hPi" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:nPi" class="def">nPi</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a><a href="src/Agda-TypeChecking-Primitive.html#nPi" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:varM" class="def">varM</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a><a href="src/Agda-TypeChecking-Primitive.html#varM" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:gApply" class="def">gApply</a> :: <a href="Agda-Syntax-Common.html#t:Hiding">Hiding</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a><a href="src/Agda-TypeChecking-Primitive.html#gApply" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:-60--64--62-" class="def">(<@>)</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a><a href="src/Agda-TypeChecking-Primitive.html#%3C%40%3E" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:-60--35--62-" class="def">(<#>)</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a><a href="src/Agda-TypeChecking-Primitive.html#%3C%23%3E" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:list" class="def">list</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a><a href="src/Agda-TypeChecking-Primitive.html#list" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:io" class="def">io</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a><a href="src/Agda-TypeChecking-Primitive.html#io" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:el" class="def">el</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a><a href="src/Agda-TypeChecking-Primitive.html#el" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:tset" class="def">tset</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a><a href="src/Agda-TypeChecking-Primitive.html#tset" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:argN" class="def">argN</a> :: e -> <a href="Agda-Syntax-Common.html#t:Arg">Arg</a> e<a href="src/Agda-TypeChecking-Primitive.html#argN" class="link">Source</a></p><div class="doc"><p>Abbreviation: <code>argN = <code><a href="Agda-Syntax-Common.html#t:Arg">Arg</a></code> <code><a href="Agda-Syntax-Common.html#v:NotHidden">NotHidden</a></code> <code><a href="Agda-Syntax-Common.html#v:Relevant">Relevant</a></code></code>.
</p></div></div><div class="top"><p class="src"><a name="v:domN" class="def">domN</a> :: e -> <a href="Agda-Syntax-Common.html#t:Dom">Dom</a> e<a href="src/Agda-TypeChecking-Primitive.html#domN" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:argH" class="def">argH</a> :: e -> <a href="Agda-Syntax-Common.html#t:Arg">Arg</a> e<a href="src/Agda-TypeChecking-Primitive.html#argH" class="link">Source</a></p><div class="doc"><p>Abbreviation: <code>argH = <code><a href="Agda-Syntax-Common.html#t:Arg">Arg</a></code> <code><a href="Agda-Syntax-Common.html#v:Hidden">Hidden</a></code> <code><a href="Agda-Syntax-Common.html#v:Relevant">Relevant</a></code></code>.
</p></div></div><div class="top"><p class="src"><a name="v:domH" class="def">domH</a> :: e -> <a href="Agda-Syntax-Common.html#t:Dom">Dom</a> e<a href="src/Agda-TypeChecking-Primitive.html#domH" class="link">Source</a></p></div><h1 id="g:2">The actual primitive functions
</h1><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:Op" class="def">Op</a> a = a -> a -> a<a href="src/Agda-TypeChecking-Primitive.html#Op" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:Fun" class="def">Fun</a> a = a -> a<a href="src/Agda-TypeChecking-Primitive.html#Fun" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:Rel" class="def">Rel</a> a = a -> a -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a><a href="src/Agda-TypeChecking-Primitive.html#Rel" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:Pred" class="def">Pred</a> a = a -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a><a href="src/Agda-TypeChecking-Primitive.html#Pred" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:primitiveFunctions" class="def">primitiveFunctions</a> :: <a href="/usr/share/doc/ghc/html/libraries/containers-0.4.2.1/Data-Map.html#t:Map">Map</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> (<a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-Primitive.html#t:PrimitiveImpl">PrimitiveImpl</a>)<a href="src/Agda-TypeChecking-Primitive.html#primitiveFunctions" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:lookupPrimitiveFunction" class="def">lookupPrimitiveFunction</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-Primitive.html#t:PrimitiveImpl">PrimitiveImpl</a><a href="src/Agda-TypeChecking-Primitive.html#lookupPrimitiveFunction" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:lookupPrimitiveFunctionQ" class="def">lookupPrimitiveFunctionQ</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a>, <a href="Agda-TypeChecking-Primitive.html#t:PrimitiveImpl">PrimitiveImpl</a>)<a href="src/Agda-TypeChecking-Primitive.html#lookupPrimitiveFunctionQ" class="link">Source</a></p></div></div></div><div id="footer"><p>Produced by <a href="http://www.haskell.org/haddock/">Haddock</a> version 2.11.0</p></div></body></html>
