<!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.Compiler.MAlonzo.Compiler</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-Compiler-MAlonzo-Compiler.html");};
//]]>
</script></head><body><div id="package-header"><ul class="links" id="page-menu"><li><a href="src/Agda-Compiler-MAlonzo-Compiler.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.Compiler.MAlonzo.Compiler</p></div><div id="synopsis"><p id="control.syn" class="caption expander" onclick="toggleSection('syn')">Synopsis</p><ul id="section.syn" class="hide" onclick="toggleSection('syn')"><li class="src short"><a href="#v:compilerMain">compilerMain</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:Interface">Interface</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:compile">compile</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:Interface">Interface</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:imports">imports</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> [<a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:ImportDecl">ImportDecl</a>]</li><li class="src short"><a href="#v:definitions">definitions</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:Definitions">Definitions</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> [<a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:Decl">Decl</a>]</li><li class="src short"><a href="#v:definition">definition</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> <a href="Agda-TypeChecking-Monad-Builtin.html#t:CoinductionKit">CoinductionKit</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:Definition">Definition</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> [<a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:Decl">Decl</a>]</li><li class="src short"><a href="#v:checkConstructorType">checkConstructorType</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/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:Decl">Decl</a>]</li><li class="src short"><a href="#v:checkCover">checkCover</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:HaskellType">HaskellType</a> -> <a href="Agda-Syntax-Common.html#t:Nat">Nat</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/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:Decl">Decl</a>]</li><li class="src short"><a href="#v:conArityAndPars">conArityAndPars</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="Agda-Syntax-Common.html#t:Nat">Nat</a>, <a href="Agda-Syntax-Common.html#t:Nat">Nat</a>)</li><li class="src short"><a href="#v:clause">clause</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> (<a href="Agda-Syntax-Common.html#t:Nat">Nat</a>, <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a>, <a href="Agda-Syntax-Internal.html#t:Clause">Clause</a>) -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:Decl">Decl</a></li><li class="src short"><a href="#v:argpatts">argpatts</a> :: [<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> <a href="Agda-Syntax-Internal.html#t:Pattern">Pattern</a>] -> [<a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:Pat">Pat</a>] -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> [<a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:Pat">Pat</a>]</li><li class="src short"><a href="#v:clausebody">clausebody</a> :: <a href="Agda-Syntax-Internal.html#t:ClauseBody">ClauseBody</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:Exp">Exp</a></li><li class="src short"><a href="#v:term">term</a> :: <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="/usr/share/doc/ghc/html/libraries/mtl-2.1.2/Control-Monad-Reader.html#t:ReaderT">ReaderT</a> <a href="Agda-Syntax-Common.html#t:Nat">Nat</a> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:Exp">Exp</a></li><li class="src short"><a href="#v:term-39-">term'</a> :: <a href="Agda-Syntax-Common.html#t:Arg">Arg</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="/usr/share/doc/ghc/html/libraries/mtl-2.1.2/Control-Monad-Reader.html#t:ReaderT">ReaderT</a> <a href="Agda-Syntax-Common.html#t:Nat">Nat</a> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:Exp">Exp</a></li><li class="src short"><a href="#v:literal">literal</a> :: <a href="Agda-Syntax-Literal.html#t:Literal">Literal</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:Exp">Exp</a></li><li class="src short"><a href="#v:hslit">hslit</a> :: <a href="Agda-Syntax-Literal.html#t:Literal">Literal</a> -> <a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:Literal">Literal</a></li><li class="src short"><a href="#v:litqname">litqname</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/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:Exp">Exp</a></li><li class="src short"><a href="#v:condecl">condecl</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="Agda-Syntax-Common.html#t:Nat">Nat</a>, <a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:ConDecl">ConDecl</a>)</li><li class="src short"><a href="#v:cdecl">cdecl</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-Syntax-Common.html#t:Nat">Nat</a> -> <a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:ConDecl">ConDecl</a></li><li class="src short"><a href="#v:tvaldecl">tvaldecl</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-Syntax-Common.html#t:Induction">Induction</a> -> <a href="Agda-Syntax-Common.html#t:Nat">Nat</a> -> <a href="Agda-Syntax-Common.html#t:Nat">Nat</a> -> [<a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:ConDecl">ConDecl</a>] -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> <a href="Agda-Syntax-Internal.html#t:Clause">Clause</a> -> [<a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:Decl">Decl</a>]</li><li class="src short"><a href="#v:infodecl">infodecl</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:Decl">Decl</a></li><li class="src short"><a href="#v:hsCast">hsCast</a> :: <a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:Exp">Exp</a> -> <a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:Exp">Exp</a></li><li class="src short"><a href="#v:hsCast-39-">hsCast'</a> :: <a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:Exp">Exp</a> -> <a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:Exp">Exp</a></li><li class="src short"><a href="#v:hsCoerce">hsCoerce</a> :: <a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:Exp">Exp</a> -> <a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:Exp">Exp</a></li><li class="src short"><a href="#v:writeModule">writeModule</a> :: <a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:Module">Module</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:rteModule">rteModule</a> :: <a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:Module">Module</a></li><li class="src short"><a href="#v:explicitForAll">explicitForAll</a> :: <a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Extension.html#t:Extension">Extension</a></li><li class="src short"><a href="#v:compileDir">compileDir</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/System-IO.html#t:FilePath">FilePath</a></li><li class="src short"><a href="#v:outFile-39-">outFile'</a> :: (<a href="/usr/share/doc/ghc/html/libraries/geniplate-0.6.0.3/Data-Generics-Geniplate.html#t:TransformBi">TransformBi</a> <a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:ModuleName">ModuleName</a> (<a href="Agda-Compiler-MAlonzo-Pretty.html#t:Wrap">Wrap</a> a), <a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Pretty.html#t:Pretty">Pretty</a> a) => a -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCMT">TCMT</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:IO">IO</a> (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:FilePath">FilePath</a>, <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:FilePath">FilePath</a>)</li><li class="src short"><a href="#v:outFile">outFile</a> :: <a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:ModuleName">ModuleName</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/System-IO.html#t:FilePath">FilePath</a></li><li class="src short"><a href="#v:outFile_">outFile_</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/System-IO.html#t:FilePath">FilePath</a></li><li class="src short"><a href="#v:callGHC">callGHC</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:Interface">Interface</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></ul></div><div id="interface"><h1>Documentation</h1><div class="top"><p class="src"><a name="v:compilerMain" class="def">compilerMain</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:Interface">Interface</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><a href="src/Agda-Compiler-MAlonzo-Compiler.html#compilerMain" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:compile" class="def">compile</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:Interface">Interface</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><a href="src/Agda-Compiler-MAlonzo-Compiler.html#compile" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:imports" class="def">imports</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> [<a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:ImportDecl">ImportDecl</a>]<a href="src/Agda-Compiler-MAlonzo-Compiler.html#imports" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:definitions" class="def">definitions</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:Definitions">Definitions</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> [<a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:Decl">Decl</a>]<a href="src/Agda-Compiler-MAlonzo-Compiler.html#definitions" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:definition" class="def">definition</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> <a href="Agda-TypeChecking-Monad-Builtin.html#t:CoinductionKit">CoinductionKit</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:Definition">Definition</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> [<a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:Decl">Decl</a>]<a href="src/Agda-Compiler-MAlonzo-Compiler.html#definition" class="link">Source</a></p><div class="doc"><p>Note that the INFINITY, SHARP and FLAT builtins are translated as
follows (if a <code><a href="Agda-TypeChecking-Monad-Builtin.html#t:CoinductionKit">CoinductionKit</a></code> is given):
</p><pre>
type Infinity a b = b
sharp :: a -> a
sharp x = x
flat :: a -> a
flat x = x
</pre></div></div><div class="top"><p class="src"><a name="v:checkConstructorType" class="def">checkConstructorType</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/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:Decl">Decl</a>]<a href="src/Agda-Compiler-MAlonzo-Compiler.html#checkConstructorType" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:checkCover" class="def">checkCover</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:HaskellType">HaskellType</a> -> <a href="Agda-Syntax-Common.html#t:Nat">Nat</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/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:Decl">Decl</a>]<a href="src/Agda-Compiler-MAlonzo-Compiler.html#checkCover" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:conArityAndPars" class="def">conArityAndPars</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="Agda-Syntax-Common.html#t:Nat">Nat</a>, <a href="Agda-Syntax-Common.html#t:Nat">Nat</a>)<a href="src/Agda-Compiler-MAlonzo-Compiler.html#conArityAndPars" class="link">Source</a></p><div class="doc"><p>Move somewhere else!
</p></div></div><div class="top"><p class="src"><a name="v:clause" class="def">clause</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> (<a href="Agda-Syntax-Common.html#t:Nat">Nat</a>, <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a>, <a href="Agda-Syntax-Internal.html#t:Clause">Clause</a>) -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:Decl">Decl</a><a href="src/Agda-Compiler-MAlonzo-Compiler.html#clause" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:argpatts" class="def">argpatts</a> :: [<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> <a href="Agda-Syntax-Internal.html#t:Pattern">Pattern</a>] -> [<a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:Pat">Pat</a>] -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> [<a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:Pat">Pat</a>]<a href="src/Agda-Compiler-MAlonzo-Compiler.html#argpatts" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:clausebody" class="def">clausebody</a> :: <a href="Agda-Syntax-Internal.html#t:ClauseBody">ClauseBody</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:Exp">Exp</a><a href="src/Agda-Compiler-MAlonzo-Compiler.html#clausebody" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:term" class="def">term</a> :: <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="/usr/share/doc/ghc/html/libraries/mtl-2.1.2/Control-Monad-Reader.html#t:ReaderT">ReaderT</a> <a href="Agda-Syntax-Common.html#t:Nat">Nat</a> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:Exp">Exp</a><a href="src/Agda-Compiler-MAlonzo-Compiler.html#term" class="link">Source</a></p><div class="doc"><p>Extract Agda term to Haskell expression.
Irrelevant arguments are extracted as <code>()</code>.
Types are extracted as <code>()</code>.
<code>DontCare</code> outside of irrelevant arguments is extracted as <code>error</code>.
</p></div></div><div class="top"><p class="src"><a name="v:term-39-" class="def">term'</a> :: <a href="Agda-Syntax-Common.html#t:Arg">Arg</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a> -> <a href="/usr/share/doc/ghc/html/libraries/mtl-2.1.2/Control-Monad-Reader.html#t:ReaderT">ReaderT</a> <a href="Agda-Syntax-Common.html#t:Nat">Nat</a> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:Exp">Exp</a><a href="src/Agda-Compiler-MAlonzo-Compiler.html#term%27" class="link">Source</a></p><div class="doc"><p>Irrelevant arguments are replaced by Haskells' ().
</p></div></div><div class="top"><p class="src"><a name="v:literal" class="def">literal</a> :: <a href="Agda-Syntax-Literal.html#t:Literal">Literal</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:Exp">Exp</a><a href="src/Agda-Compiler-MAlonzo-Compiler.html#literal" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:hslit" class="def">hslit</a> :: <a href="Agda-Syntax-Literal.html#t:Literal">Literal</a> -> <a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:Literal">Literal</a><a href="src/Agda-Compiler-MAlonzo-Compiler.html#hslit" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:litqname" class="def">litqname</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/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:Exp">Exp</a><a href="src/Agda-Compiler-MAlonzo-Compiler.html#litqname" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:condecl" class="def">condecl</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="Agda-Syntax-Common.html#t:Nat">Nat</a>, <a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:ConDecl">ConDecl</a>)<a href="src/Agda-Compiler-MAlonzo-Compiler.html#condecl" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:cdecl" class="def">cdecl</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-Syntax-Common.html#t:Nat">Nat</a> -> <a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:ConDecl">ConDecl</a><a href="src/Agda-Compiler-MAlonzo-Compiler.html#cdecl" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:tvaldecl" class="def">tvaldecl</a><a href="src/Agda-Compiler-MAlonzo-Compiler.html#tvaldecl" class="link">Source</a></p><div class="subs arguments"><p class="caption">Arguments</p><table><tr><td class="src">:: <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-Syntax-Common.html#t:Induction">Induction</a></td><td class="doc"><p>Is the type inductive or coinductive?
</p></td></tr><tr><td class="src">-> <a href="Agda-Syntax-Common.html#t:Nat">Nat</a></td><td class="doc empty"> </td></tr><tr><td class="src">-> <a href="Agda-Syntax-Common.html#t:Nat">Nat</a></td><td class="doc empty"> </td></tr><tr><td class="src">-> [<a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:ConDecl">ConDecl</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-Maybe.html#t:Maybe">Maybe</a> <a href="Agda-Syntax-Internal.html#t:Clause">Clause</a></td><td class="doc empty"> </td></tr><tr><td class="src">-> [<a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:Decl">Decl</a>]</td><td class="doc empty"> </td></tr></table></div></div><div class="top"><p class="src"><a name="v:infodecl" class="def">infodecl</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:Decl">Decl</a><a href="src/Agda-Compiler-MAlonzo-Compiler.html#infodecl" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:hsCast" class="def">hsCast</a> :: <a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:Exp">Exp</a> -> <a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:Exp">Exp</a><a href="src/Agda-Compiler-MAlonzo-Compiler.html#hsCast" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:hsCast-39-" class="def">hsCast'</a> :: <a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:Exp">Exp</a> -> <a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:Exp">Exp</a><a href="src/Agda-Compiler-MAlonzo-Compiler.html#hsCast%27" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:hsCoerce" class="def">hsCoerce</a> :: <a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:Exp">Exp</a> -> <a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:Exp">Exp</a><a href="src/Agda-Compiler-MAlonzo-Compiler.html#hsCoerce" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:writeModule" class="def">writeModule</a> :: <a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:Module">Module</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><a href="src/Agda-Compiler-MAlonzo-Compiler.html#writeModule" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:rteModule" class="def">rteModule</a> :: <a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:Module">Module</a><a href="src/Agda-Compiler-MAlonzo-Compiler.html#rteModule" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:explicitForAll" class="def">explicitForAll</a> :: <a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Extension.html#t:Extension">Extension</a><a href="src/Agda-Compiler-MAlonzo-Compiler.html#explicitForAll" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:compileDir" class="def">compileDir</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/System-IO.html#t:FilePath">FilePath</a><a href="src/Agda-Compiler-MAlonzo-Compiler.html#compileDir" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:outFile-39-" class="def">outFile'</a> :: (<a href="/usr/share/doc/ghc/html/libraries/geniplate-0.6.0.3/Data-Generics-Geniplate.html#t:TransformBi">TransformBi</a> <a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:ModuleName">ModuleName</a> (<a href="Agda-Compiler-MAlonzo-Pretty.html#t:Wrap">Wrap</a> a), <a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Pretty.html#t:Pretty">Pretty</a> a) => a -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCMT">TCMT</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:IO">IO</a> (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:FilePath">FilePath</a>, <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:FilePath">FilePath</a>)<a href="src/Agda-Compiler-MAlonzo-Compiler.html#outFile%27" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:outFile" class="def">outFile</a> :: <a href="/usr/share/doc/ghc/html/libraries/haskell-src-exts-1.13.5/Language-Haskell-Exts-Syntax.html#t:ModuleName">ModuleName</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/System-IO.html#t:FilePath">FilePath</a><a href="src/Agda-Compiler-MAlonzo-Compiler.html#outFile" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:outFile_" class="def">outFile_</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/System-IO.html#t:FilePath">FilePath</a><a href="src/Agda-Compiler-MAlonzo-Compiler.html#outFile_" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:callGHC" class="def">callGHC</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:Interface">Interface</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><a href="src/Agda-Compiler-MAlonzo-Compiler.html#callGHC" 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>
