<!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.Serialise</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-Serialise.html");};
//]]>
</script></head><body><div id="package-header"><ul class="links" id="page-menu"><li><a href="src/Agda-TypeChecking-Serialise.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.Serialise</p></div><div id="description"><p class="caption">Description</p><div class="doc"><p>Structure-sharing serialisation of Agda interface files.
</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:encode">encode</a> :: <a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> a => a -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/bytestring-0.9.2.1/Data-ByteString-Lazy.html#t:ByteString">ByteString</a></li><li class="src short"><a href="#v:encodeFile">encodeFile</a> :: <a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> a => <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:FilePath">FilePath</a> -> a -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a></li><li class="src short"><a href="#v:decode">decode</a> :: <a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> a => <a href="/usr/share/doc/ghc/html/libraries/bytestring-0.9.2.1/Data-ByteString-Lazy.html#t:ByteString">ByteString</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> a)</li><li class="src short"><a href="#v:decodeFile">decodeFile</a> :: <a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> a => <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:FilePath">FilePath</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> a)</li><li class="src short"><span class="keyword">class</span> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Typeable-Internal.html#t:Typeable">Typeable</a> a => <a href="#t:EmbPrj">EmbPrj</a> a </li></ul></div><div id="interface"><h1>Documentation</h1><div class="top"><p class="src"><a name="v:encode" class="def">encode</a> :: <a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> a => a -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/bytestring-0.9.2.1/Data-ByteString-Lazy.html#t:ByteString">ByteString</a><a href="src/Agda-TypeChecking-Serialise.html#encode" class="link">Source</a></p><div class="doc"><p>Encodes something. To ensure relocatability file paths in
positions are replaced with module names.
</p></div></div><div class="top"><p class="src"><a name="v:encodeFile" class="def">encodeFile</a><a href="src/Agda-TypeChecking-Serialise.html#encodeFile" class="link">Source</a></p><div class="subs arguments"><p class="caption">Arguments</p><table><tr><td class="src">:: <a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> a</td><td class="doc empty"> </td></tr><tr><td class="src">=> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:FilePath">FilePath</a></td><td class="doc"><p>The encoded data is written to this file.
</p></td></tr><tr><td class="src">-> a</td><td class="doc"><p>Something.
</p></td></tr><tr><td class="src">-> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a></td><td class="doc empty"> </td></tr></table></div><div class="doc"><p>Encodes something. To ensure relocatability file paths in
positions are replaced with module names.
</p></div></div><div class="top"><p class="src"><a name="v:decode" class="def">decode</a> :: <a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> a => <a href="/usr/share/doc/ghc/html/libraries/bytestring-0.9.2.1/Data-ByteString-Lazy.html#t:ByteString">ByteString</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> a)<a href="src/Agda-TypeChecking-Serialise.html#decode" class="link">Source</a></p><div class="doc"><p>Decodes something. The result depends on the include path.
</p><p>Returns <code><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#v:Nothing">Nothing</a></code> if the input does not start with the right magic
number or some other decoding error is encountered.
</p></div></div><div class="top"><p class="src"><a name="v:decodeFile" class="def">decodeFile</a> :: <a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> a => <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:FilePath">FilePath</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> a)<a href="src/Agda-TypeChecking-Serialise.html#decodeFile" class="link">Source</a></p><div class="doc"><p>Decodes something. The result depends on the include path.
</p><p>Returns <code><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#v:Nothing">Nothing</a></code> if the file does not start with the right magic
number or some other decoding error is encountered.
</p></div></div><div class="top"><p class="src"><span class="keyword">class</span> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Typeable-Internal.html#t:Typeable">Typeable</a> a => <a name="t:EmbPrj" class="def">EmbPrj</a> a <a href="src/Agda-TypeChecking-Serialise.html#EmbPrj" class="link">Source</a></p><div class="subs instances"><p id="control.i:EmbPrj" class="caption collapser" onclick="toggleSection('i:EmbPrj')">Instances</p><div id="section.i:EmbPrj" class="show"><table><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</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-Serialise.html#t:EmbPrj">EmbPrj</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-Serialise.html#t:EmbPrj">EmbPrj</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-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int32">Int32</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</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-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> ()</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Utils-Permutation.html#t:Permutation">Permutation</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Utils-FileName.html#t:AbsolutePath">AbsolutePath</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Position.html#t:Range">Range</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Position.html#t:Interval">Interval</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Position.html#t:Position">Position</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Common.html#t:NameId">NameId</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Common.html#t:IsAbstract">IsAbstract</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Common.html#t:Access">Access</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Common.html#t:Relevance">Relevance</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Common.html#t:Hiding">Hiding</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Common.html#t:Induction">Induction</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Common.html#t:Delayed">Delayed</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Compiler-JS-Syntax.html#t:MemberId">MemberId</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Compiler-JS-Syntax.html#t:GlobalId">GlobalId</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Compiler-JS-Syntax.html#t:LocalId">LocalId</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Compiler-JS-Syntax.html#t:Exp">Exp</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Concrete-Name.html#t:TopLevelModuleName">TopLevelModuleName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Concrete-Name.html#t:NamePart">NamePart</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Interaction-Highlighting-Range.html#t:Range">Range</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Notation.html#t:GenPart">GenPart</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Fixity.html#t:Precedence">Precedence</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Fixity.html#t:Fixity">Fixity</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Fixity.html#t:Fixity-39-">Fixity'</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Abstract-Name.html#t:AmbiguousQName">AmbiguousQName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</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-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Literal.html#t:Literal">Literal</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Interaction-Highlighting-Precise.html#t:CompressedFile">CompressedFile</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Interaction-Highlighting-Precise.html#t:MetaInfo">MetaInfo</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Interaction-Highlighting-Precise.html#t:OtherAspect">OtherAspect</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Interaction-Highlighting-Precise.html#t:NameKind">NameKind</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Interaction-Highlighting-Precise.html#t:Aspect">Aspect</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Scope-Base.html#t:AbstractModule">AbstractModule</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Scope-Base.html#t:AbstractName">AbstractName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Scope-Base.html#t:KindOfName">KindOfName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Scope-Base.html#t:NameSpace">NameSpace</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Scope-Base.html#t:ScopeInfo">ScopeInfo</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Scope-Base.html#t:NameSpaceId">NameSpaceId</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Internal.html#t:Pattern">Pattern</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Internal.html#t:ClauseBody">ClauseBody</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Internal.html#t:Clause">Clause</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Internal.html#t:LevelAtom">LevelAtom</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Internal.html#t:PlusLevel">PlusLevel</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Internal.html#t:Level">Level</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Internal.html#t:Sort">Sort</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Internal.html#t:Telescope">Telescope</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</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-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Compiler-Epic-Interface.html#t:EInterface">EInterface</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Compiler-Epic-Interface.html#t:InjectiveFun">InjectiveFun</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Compiler-Epic-Interface.html#t:Relevance">Relevance</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Compiler-Epic-Interface.html#t:Forced">Forced</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Compiler-Epic-Interface.html#t:Tag">Tag</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-TypeChecking-CompiledClause.html#t:CompiledClauses">CompiledClauses</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Abstract.html#t:Pattern">Pattern</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Abstract.html#t:TypedBinding">TypedBinding</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Abstract.html#t:TypedBindings">TypedBindings</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Abstract.html#t:LamBinding">LamBinding</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Abstract.html#t:LetBinding">LetBinding</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Abstract.html#t:Expr">Expr</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-TypeChecking-Monad-Base.html#t:CtxId">CtxId</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-TypeChecking-Monad-Base.html#t:MutualId">MutualId</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-TypeChecking-Monad-Base.html#t:TermHead">TermHead</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-TypeChecking-Monad-Base.html#t:FunctionInverse">FunctionInverse</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-TypeChecking-Monad-Base.html#t:Defn">Defn</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-TypeChecking-Monad-Base.html#t:Occurrence">Occurrence</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-TypeChecking-Monad-Base.html#t:CompiledRepresentation">CompiledRepresentation</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-TypeChecking-Monad-Base.html#t:Polarity">Polarity</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-TypeChecking-Monad-Base.html#t:HaskellRepresentation">HaskellRepresentation</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-TypeChecking-Monad-Base.html#t:Definition">Definition</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-TypeChecking-Monad-Base.html#t:DisplayTerm">DisplayTerm</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-TypeChecking-Monad-Base.html#t:DisplayForm">DisplayForm</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-TypeChecking-Monad-Base.html#t:Section">Section</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-TypeChecking-Monad-Base.html#t:Signature">Signature</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-TypeChecking-Monad-Base.html#t:Interface">Interface</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> a => <a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> [a]</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> a => <a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src">(<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Ord.html#t:Ord">Ord</a> a, <a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> a) => <a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> (<a href="/usr/share/doc/ghc/html/libraries/containers-0.4.2.1/Data-Set.html#t:Set">Set</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> a => <a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> a => <a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> (<a href="Agda-Syntax-Common.html#t:Dom">Dom</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> a => <a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> (<a href="Agda-Syntax-Internal.html#t:Abs">Abs</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> a => <a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> (<a href="Agda-TypeChecking-CompiledClause.html#t:Case">Case</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> a => <a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> (<a href="Agda-TypeChecking-CompiledClause.html#t:WithArity">WithArity</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> a => <a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> (<a href="Agda-TypeChecking-Monad-Base.html#t:Builtin">Builtin</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> a => <a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> (<a href="Agda-TypeChecking-Monad-Base.html#t:Open">Open</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src">(<a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> a, <a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> b) => <a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> (a, b)</td><td class="doc empty"> </td></tr><tr><td class="src">(<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Ord.html#t:Ord">Ord</a> a, <a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> a, <a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> b) => <a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> (<a href="/usr/share/doc/ghc/html/libraries/containers-0.4.2.1/Data-Map.html#t:Map">Map</a> a b)</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> k, <a href="/usr/share/doc/ghc/html/libraries/hashable-1.1.2.5/Data-Hashable.html#t:Hashable">Hashable</a> k, <a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> k, <a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> v) => <a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> (<a href="/usr/share/doc/ghc/html/libraries/unordered-containers-0.2.2.1/Data-HashMap-Strict.html#t:HashMap">HashMap</a> k v)</td><td class="doc empty"> </td></tr><tr><td class="src">(<a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> s, <a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> t) => <a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> (<a href="Agda-Syntax-Common.html#t:Named">Named</a> s t)</td><td class="doc empty"> </td></tr><tr><td class="src">(<a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> a, <a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> b, <a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> c) => <a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> (a, b, c)</td><td class="doc empty"> </td></tr></table></div></div></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>
