https://github.com/AU-COBRA/ConCert
Tip revision: 932cb97084707cbac70c60db5d249bee24626750 authored by github-actions[bot] on 22 August 2022, 09:00:22 UTC
Deploy to GitHub pages
Deploy to GitHub pages
Tip revision: 932cb97
ConCert.Extraction.PrettyPrinterMonad.html
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html;charset=utf-8" />
<meta name="viewport" content="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no" />
<link href="coqdoc.css" rel="stylesheet" type="text/css" />
<link href="coqdocjs.css" rel="stylesheet" type="text/css"/>
<link href="toc.css" rel="stylesheet" type="text/css"/>
<script type="text/javascript" src="config.js"></script>
<script type="text/javascript" src="coqdocjs.js"></script>
</head>
<body onload="document.getElementById('content').focus()">
<div id="header">
<span class="left">
<span class="modulename"> <script> document.write(document.title) </script> </span>
<span id="toggle-toc">Contents</span>
</span>
<span class="button" id="toggle-proofs"></span>
<span class="right">
<a href="https://github.com/AU-COBRA/ConCert" target="_balnk">Project Page</a>
<a href="index.html">Index</a>
<a href="toc.html">Table of contents</a>
</span>
</div>
<div id="content" tabindex="-1" onblur="document.getElementById('content').focus()">
<div id="js-toc" class="toc" data-toc="h1,h2,h3,h4" data-toc-container="doc" data-toc-offset="-40">
<div id="js-toc-header" class="toc-header">Contents:</div>
</div>
<div id="main">
<h1 class="libtitle">Library ConCert.Extraction.PrettyPrinterMonad</h1>
<div class="code">
<span class="id" title="keyword">From</span> <span class="id" title="var">Coq</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#"><span class="id" title="library">List</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">Coq</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Strings.Ascii.html#"><span class="id" title="library">Ascii</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">Coq</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Strings.String.html#"><span class="id" title="library">String</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">MetaCoq.Template</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.monad_utils.html#"><span class="id" title="library">monad_utils</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">MetaCoq.SafeChecker</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.SafeChecker.PCUICErrors.html#"><span class="id" title="library">PCUICErrors</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">ConCert.Extraction</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="ConCert.Extraction.ResultMonad.html#"><span class="id" title="library">ResultMonad</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">ConCert.Extraction</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="ConCert.Extraction.Common.html#"><span class="id" title="library">Common</span></a>.<br/>
<br/>
<span class="id" title="keyword">Import</span> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.monad_utils.html#MCMonadNotation"><span class="id" title="module">monad_utils.MCMonadNotation</span></a>.<br/>
<span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#ListNotations"><span class="id" title="module">ListNotations</span></a>.<br/>
<span class="id" title="keyword">Local Open</span> <span class="id" title="keyword">Scope</span> <span class="id" title="var">string</span>.<br/>
<br/>
<span class="id" title="keyword">Import</span> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Kernames.html#"><span class="id" title="module">Kernames</span></a>.<br/>
<br/>
<span class="id" title="keyword">Record</span> <a id="PrettyPrinterState" class="idref" href="#PrettyPrinterState"><span class="id" title="record">PrettyPrinterState</span></a> :=<br/>
{<br/>
<a id="indent_stack" class="idref" href="#indent_stack"><span class="id" title="projection">indent_stack</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>;<br/>
<a id="used_names" class="idref" href="#used_names"><span class="id" title="projection">used_names</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Kernames.html#ident"><span class="id" title="definition">ident</span></a>;<br/>
<a id="output_lines" class="idref" href="#output_lines"><span class="id" title="projection">output_lines</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac4"><span class="id" title="notation">*</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>);<br/>
<a id="cur_output_line" class="idref" href="#cur_output_line"><span class="id" title="projection">cur_output_line</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac4"><span class="id" title="notation">*</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>;<br/>
}.<br/>
<br/>
<span class="id" title="keyword">Notation</span> <a id="bs_to_s" class="idref" href="#bs_to_s"><span class="id" title="abbreviation">bs_to_s</span></a> := <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.utils.bytestring.html#String.to_string"><span class="id" title="definition">bytestring.String.to_string</span></a>.<br/>
<span class="id" title="keyword">Notation</span> <a id="s_to_bs" class="idref" href="#s_to_bs"><span class="id" title="abbreviation">s_to_bs</span></a> := <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.utils.bytestring.html#String.of_string"><span class="id" title="definition">bytestring.String.of_string</span></a>.<br/>
<br/>
<span class="id" title="keyword">Local</span> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.utils.bytestring.html#String.to_string"><span class="id" title="definition">Coercion</span></a> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.utils.bytestring.html#String.to_string"><span class="id" title="definition">bs_to_s</span></a> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.utils.bytestring.html#String.to_string"><span class="id" title="definition">:</span></a> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.utils.bytestring.html#String.to_string"><span class="id" title="definition">bytestring.string</span></a> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.utils.bytestring.html#String.to_string"><span class="id" title="definition">>-></span></a> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.utils.bytestring.html#String.to_string"><span class="id" title="definition">string</span></a>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="PrettyPrinter" class="idref" href="#PrettyPrinter"><span class="id" title="definition">PrettyPrinter</span></a> <a id="A:6" class="idref" href="#A:6"><span class="id" title="binder">A</span></a> := <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#PrettyPrinterState"><span class="id" title="record">PrettyPrinterState</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="ConCert.Extraction.ResultMonad.html#result"><span class="id" title="inductive">result</span></a> (<a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#A:6"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac4"><span class="id" title="notation">*</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#PrettyPrinterState"><span class="id" title="record">PrettyPrinterState</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>.<br/>
<br/>
<span class="id" title="keyword">Instance</span> <a id="Monad_PrettyPrinter" class="idref" href="#Monad_PrettyPrinter"><span class="id" title="instance">Monad_PrettyPrinter</span></a> : <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.monad_utils.html#Monad"><span class="id" title="class">Monad</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#PrettyPrinter"><span class="id" title="definition">PrettyPrinter</span></a> :=<br/>
{| <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.monad_utils.html#ret"><span class="id" title="method">ret</span></a> <span class="id" title="var">_</span> <a id="a:7" class="idref" href="#a:7"><span class="id" title="binder">a</span></a> <a id="pps:8" class="idref" href="#pps:8"><span class="id" title="binder">pps</span></a> := <a class="idref" href="ConCert.Extraction.ResultMonad.html#Ok"><span class="id" title="constructor">Ok</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#a:7"><span class="id" title="variable">a</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#pps:8"><span class="id" title="variable">pps</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a>;<br/>
<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.monad_utils.html#bind"><span class="id" title="method">bind</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a id="m:9" class="idref" href="#m:9"><span class="id" title="binder">m</span></a> <a id="f:10" class="idref" href="#f:10"><span class="id" title="binder">f</span></a> <a id="pps:11" class="idref" href="#pps:11"><span class="id" title="binder">pps</span></a> :=<br/>
<span class="id" title="keyword">match</span> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#m:9"><span class="id" title="variable">m</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#pps:11"><span class="id" title="variable">pps</span></a> <span class="id" title="keyword">with</span><br/>
| <a class="idref" href="ConCert.Extraction.ResultMonad.html#Ok"><span class="id" title="constructor">Ok</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><span class="id" title="var">a</span><a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <span class="id" title="var">pps</span><a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a> => <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#f:10"><span class="id" title="variable">f</span></a> <span class="id" title="var">a</span> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#pps:11"><span class="id" title="variable">pps</span></a><br/>
| <a class="idref" href="ConCert.Extraction.ResultMonad.html#Err"><span class="id" title="constructor">Err</span></a> <span class="id" title="var">err</span> => <a class="idref" href="ConCert.Extraction.ResultMonad.html#Err"><span class="id" title="constructor">Err</span></a> <span class="id" title="var">err</span><br/>
<span class="id" title="keyword">end</span> |}.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="map_pps" class="idref" href="#map_pps"><span class="id" title="definition">map_pps</span></a><br/>
(<a id="f:12" class="idref" href="#f:12"><span class="id" title="binder">f</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>)<br/>
(<a id="g:13" class="idref" href="#g:13"><span class="id" title="binder">g</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Kernames.html#ident"><span class="id" title="definition">ident</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Kernames.html#ident"><span class="id" title="definition">ident</span></a>)<br/>
(<a id="h:14" class="idref" href="#h:14"><span class="id" title="binder">h</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac4"><span class="id" title="notation">*</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac4"><span class="id" title="notation">*</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>))<br/>
(<a id="i:15" class="idref" href="#i:15"><span class="id" title="binder">i</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac4"><span class="id" title="notation">*</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac4"><span class="id" title="notation">*</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) : <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#PrettyPrinter"><span class="id" title="definition">PrettyPrinter</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a> :=<br/>
<span class="id" title="keyword">fun</span> <a id="pps:16" class="idref" href="#pps:16"><span class="id" title="binder">pps</span></a> =><br/>
<a class="idref" href="ConCert.Extraction.ResultMonad.html#Ok"><span class="id" title="constructor">Ok</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#tt"><span class="id" title="constructor">tt</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a><br/>
<span class="id" title="keyword">let</span> (<a id="a:17" class="idref" href="#a:17"><span class="id" title="binder">a</span></a>, <a id="b:18" class="idref" href="#b:18"><span class="id" title="binder">b</span></a>, <a id="c:19" class="idref" href="#c:19"><span class="id" title="binder">c</span></a>, <a id="d:20" class="idref" href="#d:20"><span class="id" title="binder">d</span></a>) := <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#pps:16"><span class="id" title="variable">pps</span></a> <span class="id" title="tactic">in</span><br/>
<a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#Build_PrettyPrinterState"><span class="id" title="constructor">Build_PrettyPrinterState</span></a> (<a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#f:12"><span class="id" title="variable">f</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#a:17"><span class="id" title="variable">a</span></a>) (<a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#g:13"><span class="id" title="variable">g</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#b:18"><span class="id" title="variable">b</span></a>) (<a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#h:14"><span class="id" title="variable">h</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#c:19"><span class="id" title="variable">c</span></a>) (<a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#i:15"><span class="id" title="variable">i</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#d:20"><span class="id" title="variable">d</span></a>)<a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a>.<br/>
<br/>
<span class="id" title="keyword">Fixpoint</span> <a id="prefix_spaces" class="idref" href="#prefix_spaces"><span class="id" title="definition">prefix_spaces</span></a> <a id="n:21" class="idref" href="#n:21"><span class="id" title="binder">n</span></a> <a id="s:22" class="idref" href="#s:22"><span class="id" title="binder">s</span></a> :=<br/>
<span class="id" title="keyword">match</span> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#n:21"><span class="id" title="variable">n</span></a> <span class="id" title="keyword">with</span><br/>
| 0 => <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#s:22"><span class="id" title="variable">s</span></a><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <span class="id" title="var">n</span> => <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#prefix_spaces:23"><span class="id" title="definition">prefix_spaces</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#n:21"><span class="id" title="variable">n</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Strings.String.html#String"><span class="id" title="constructor">String</span></a> " "%<span class="id" title="var">char</span> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#s:22"><span class="id" title="variable">s</span></a>)<br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="collect_output_lines" class="idref" href="#collect_output_lines"><span class="id" title="definition">collect_output_lines</span></a> <a id="pps:25" class="idref" href="#pps:25"><span class="id" title="binder">pps</span></a> :=<br/>
<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.utils.MCList.html#rev_map"><span class="id" title="definition">MCList.rev_map</span></a> (<span class="id" title="keyword">fun</span> '<a id="pat:28" class="idref" href="#pat:28"><span class="id" title="binder">(</span></a><a id="pat:28" class="idref" href="#pat:28"><span class="id" title="binder">n</span></a><a id="pat:28" class="idref" href="#pat:28"><span class="id" title="binder">,</span></a> <a id="pat:28" class="idref" href="#pat:28"><span class="id" title="binder">l</span></a><a id="pat:28" class="idref" href="#pat:28"><span class="id" title="binder">)</span></a> => <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#prefix_spaces"><span class="id" title="definition">prefix_spaces</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#n:27"><span class="id" title="variable">n</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#l:26"><span class="id" title="variable">l</span></a>) (<a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#cur_output_line"><span class="id" title="projection">cur_output_line</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#pps:25"><span class="id" title="variable">pps</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#::list_scope:x_'::'_x"><span class="id" title="notation">::</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#output_lines"><span class="id" title="projection">output_lines</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#pps:25"><span class="id" title="variable">pps</span></a>).<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="result_string_err" class="idref" href="#result_string_err"><span class="id" title="definition">result_string_err</span></a> <a id="A:29" class="idref" href="#A:29"><span class="id" title="binder">A</span></a> := <a class="idref" href="ConCert.Extraction.ResultMonad.html#result"><span class="id" title="inductive">result</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#A:29"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="finish_print_lines" class="idref" href="#finish_print_lines"><span class="id" title="definition">finish_print_lines</span></a> {<a id="A:30" class="idref" href="#A:30"><span class="id" title="binder">A</span></a>} (<a id="pp:31" class="idref" href="#pp:31"><span class="id" title="binder">pp</span></a> : <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#PrettyPrinter"><span class="id" title="definition">PrettyPrinter</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#A:30"><span class="id" title="variable">A</span></a>) : <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#result_string_err"><span class="id" title="definition">result_string_err</span></a> (<a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#A:30"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac4"><span class="id" title="notation">*</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) :=<br/>
<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.monad_utils.html#254b85403bdb9d2adf407ad8f41a76a6"><span class="id" title="notation">'</span></a><a id="pat:34" class="idref" href="#pat:34"><span class="id" title="binder">(</span></a><a id="pat:34" class="idref" href="#pat:34"><span class="id" title="binder">a</span></a><a id="pat:34" class="idref" href="#pat:34"><span class="id" title="binder">,</span></a> <a id="pat:34" class="idref" href="#pat:34"><span class="id" title="binder">pps</span></a><a id="pat:34" class="idref" href="#pat:34"><span class="id" title="binder">)</span></a> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.monad_utils.html#254b85403bdb9d2adf407ad8f41a76a6"><span class="id" title="notation"><-</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#pp:31"><span class="id" title="variable">pp</span></a> {| <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#indent_stack"><span class="id" title="projection">indent_stack</span></a> := <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#ae9a5e1034e143b218b09d8e454472bd"><span class="id" title="notation">[]</span></a>;<br/>
<a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#used_names"><span class="id" title="projection">used_names</span></a> := <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#ae9a5e1034e143b218b09d8e454472bd"><span class="id" title="notation">[]</span></a>;<br/>
<a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#output_lines"><span class="id" title="projection">output_lines</span></a> := <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#ae9a5e1034e143b218b09d8e454472bd"><span class="id" title="notation">[]</span></a>;<br/>
<a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#cur_output_line"><span class="id" title="projection">cur_output_line</span></a> := <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a>0<a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> ""<a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a> |}<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.monad_utils.html#254b85403bdb9d2adf407ad8f41a76a6"><span class="id" title="notation">;;</span></a><br/>
<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.monad_utils.html#ret"><span class="id" title="method">ret</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#a:33"><span class="id" title="variable">a</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#collect_output_lines"><span class="id" title="definition">collect_output_lines</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#pps:32"><span class="id" title="variable">pps</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="collect_output" class="idref" href="#collect_output"><span class="id" title="definition">collect_output</span></a> <a id="pps:35" class="idref" href="#pps:35"><span class="id" title="binder">pps</span></a> :=<br/>
<a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Strings.String.html#concat"><span class="id" title="definition">concat</span></a> <a class="idref" href="ConCert.Extraction.Common.html#nl"><span class="id" title="definition">nl</span></a> (<a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#collect_output_lines"><span class="id" title="definition">collect_output_lines</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#pps:35"><span class="id" title="variable">pps</span></a>).<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="printer_fail" class="idref" href="#printer_fail"><span class="id" title="definition">printer_fail</span></a> {<a id="A:36" class="idref" href="#A:36"><span class="id" title="binder">A</span></a>} (<a id="str:37" class="idref" href="#str:37"><span class="id" title="binder">str</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) : <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#PrettyPrinter"><span class="id" title="definition">PrettyPrinter</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#A:36"><span class="id" title="variable">A</span></a> :=<br/>
<span class="id" title="keyword">fun</span> <a id="pps:38" class="idref" href="#pps:38"><span class="id" title="binder">pps</span></a> => <a class="idref" href="ConCert.Extraction.ResultMonad.html#Err"><span class="id" title="constructor">Err</span></a> (<a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#str:37"><span class="id" title="variable">str</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Strings.String.html#169ad156fbc6036a53a0338819a2b301"><span class="id" title="notation">++</span></a> <a class="idref" href="ConCert.Extraction.Common.html#nl"><span class="id" title="definition">nl</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Strings.String.html#169ad156fbc6036a53a0338819a2b301"><span class="id" title="notation">++</span></a> "failed after printing" <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Strings.String.html#169ad156fbc6036a53a0338819a2b301"><span class="id" title="notation">++</span></a> <a class="idref" href="ConCert.Extraction.Common.html#nl"><span class="id" title="definition">nl</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Strings.String.html#169ad156fbc6036a53a0338819a2b301"><span class="id" title="notation">++</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#collect_output"><span class="id" title="definition">collect_output</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#pps:38"><span class="id" title="variable">pps</span></a>).<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="finish_print" class="idref" href="#finish_print"><span class="id" title="definition">finish_print</span></a> {<a id="A:39" class="idref" href="#A:39"><span class="id" title="binder">A</span></a>} (<a id="pp:40" class="idref" href="#pp:40"><span class="id" title="binder">pp</span></a> : <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#PrettyPrinter"><span class="id" title="definition">PrettyPrinter</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#A:39"><span class="id" title="variable">A</span></a>) : <a class="idref" href="ConCert.Extraction.ResultMonad.html#result"><span class="id" title="inductive">result</span></a> (<a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#A:39"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac4"><span class="id" title="notation">*</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a> :=<br/>
<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.monad_utils.html#254b85403bdb9d2adf407ad8f41a76a6"><span class="id" title="notation">'</span></a><a id="pat:43" class="idref" href="#pat:43"><span class="id" title="binder">(</span></a><a id="pat:43" class="idref" href="#pat:43"><span class="id" title="binder">a</span></a><a id="pat:43" class="idref" href="#pat:43"><span class="id" title="binder">,</span></a> <a id="pat:43" class="idref" href="#pat:43"><span class="id" title="binder">lines</span></a><a id="pat:43" class="idref" href="#pat:43"><span class="id" title="binder">)</span></a> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.monad_utils.html#254b85403bdb9d2adf407ad8f41a76a6"><span class="id" title="notation"><-</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#finish_print_lines"><span class="id" title="definition">finish_print_lines</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#pp:40"><span class="id" title="variable">pp</span></a><a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.monad_utils.html#254b85403bdb9d2adf407ad8f41a76a6"><span class="id" title="notation">;;</span></a><br/>
<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.monad_utils.html#ret"><span class="id" title="method">ret</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#a:42"><span class="id" title="variable">a</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Strings.String.html#concat"><span class="id" title="definition">concat</span></a> <a class="idref" href="ConCert.Extraction.Common.html#nl"><span class="id" title="definition">nl</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#lines:41"><span class="id" title="variable">lines</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="get_indent" class="idref" href="#get_indent"><span class="id" title="definition">get_indent</span></a> : <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#PrettyPrinter"><span class="id" title="definition">PrettyPrinter</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> :=<br/>
<span class="id" title="keyword">fun</span> <a id="pps:44" class="idref" href="#pps:44"><span class="id" title="binder">pps</span></a> => <a class="idref" href="ConCert.Extraction.ResultMonad.html#Ok"><span class="id" title="constructor">Ok</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#hd"><span class="id" title="definition">hd</span></a> 0 (<a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#indent_stack"><span class="id" title="projection">indent_stack</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#pps:44"><span class="id" title="variable">pps</span></a>)<a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#pps:44"><span class="id" title="variable">pps</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="map_indent_stack" class="idref" href="#map_indent_stack"><span class="id" title="definition">map_indent_stack</span></a> (<a id="f:45" class="idref" href="#f:45"><span class="id" title="binder">f</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) : <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#PrettyPrinter"><span class="id" title="definition">PrettyPrinter</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a> :=<br/>
<a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#map_pps"><span class="id" title="definition">map_pps</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#f:45"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#id"><span class="id" title="definition">id</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#id"><span class="id" title="definition">id</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#id"><span class="id" title="definition">id</span></a>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="push_indent" class="idref" href="#push_indent"><span class="id" title="definition">push_indent</span></a> (<a id="n:46" class="idref" href="#n:46"><span class="id" title="binder">n</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) : <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#PrettyPrinter"><span class="id" title="definition">PrettyPrinter</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a> :=<br/>
<a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#map_indent_stack"><span class="id" title="definition">map_indent_stack</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#cons"><span class="id" title="constructor">cons</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#n:46"><span class="id" title="variable">n</span></a>).<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="pop_indent" class="idref" href="#pop_indent"><span class="id" title="definition">pop_indent</span></a> : <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#PrettyPrinter"><span class="id" title="definition">PrettyPrinter</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a> :=<br/>
<a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#map_indent_stack"><span class="id" title="definition">map_indent_stack</span></a> (@<a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#tl"><span class="id" title="definition">tl</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>).<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="get_used_names" class="idref" href="#get_used_names"><span class="id" title="definition">get_used_names</span></a> : <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#PrettyPrinter"><span class="id" title="definition">PrettyPrinter</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Kernames.html#ident"><span class="id" title="definition">ident</span></a>) :=<br/>
<span class="id" title="keyword">fun</span> <a id="pps:47" class="idref" href="#pps:47"><span class="id" title="binder">pps</span></a> => <a class="idref" href="ConCert.Extraction.ResultMonad.html#Ok"><span class="id" title="constructor">Ok</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#used_names"><span class="id" title="projection">used_names</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#pps:47"><span class="id" title="variable">pps</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#pps:47"><span class="id" title="variable">pps</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="map_used_names" class="idref" href="#map_used_names"><span class="id" title="definition">map_used_names</span></a> (<a id="f:48" class="idref" href="#f:48"><span class="id" title="binder">f</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Kernames.html#ident"><span class="id" title="definition">ident</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Kernames.html#ident"><span class="id" title="definition">ident</span></a>) : <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#PrettyPrinter"><span class="id" title="definition">PrettyPrinter</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a> :=<br/>
<a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#map_pps"><span class="id" title="definition">map_pps</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#id"><span class="id" title="definition">id</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#f:48"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#id"><span class="id" title="definition">id</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#id"><span class="id" title="definition">id</span></a>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="push_use" class="idref" href="#push_use"><span class="id" title="definition">push_use</span></a> (<a id="n:49" class="idref" href="#n:49"><span class="id" title="binder">n</span></a> : <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Kernames.html#ident"><span class="id" title="definition">ident</span></a>) : <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#PrettyPrinter"><span class="id" title="definition">PrettyPrinter</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a> :=<br/>
<a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#map_used_names"><span class="id" title="definition">map_used_names</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#cons"><span class="id" title="constructor">cons</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#n:49"><span class="id" title="variable">n</span></a>).<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="pop_use" class="idref" href="#pop_use"><span class="id" title="definition">pop_use</span></a> : <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#PrettyPrinter"><span class="id" title="definition">PrettyPrinter</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a> :=<br/>
<a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#map_used_names"><span class="id" title="definition">map_used_names</span></a> (@<a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#tl"><span class="id" title="definition">tl</span></a> <span class="id" title="var">_</span>).<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="get_current_line_length" class="idref" href="#get_current_line_length"><span class="id" title="definition">get_current_line_length</span></a> : <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#PrettyPrinter"><span class="id" title="definition">PrettyPrinter</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> :=<br/>
<span class="id" title="keyword">fun</span> <a id="pps:50" class="idref" href="#pps:50"><span class="id" title="binder">pps</span></a> => <a class="idref" href="ConCert.Extraction.ResultMonad.html#Ok"><span class="id" title="constructor">Ok</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#fst"><span class="id" title="definition">fst</span></a> (<a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#cur_output_line"><span class="id" title="projection">cur_output_line</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#pps:50"><span class="id" title="variable">pps</span></a>)<a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Strings.String.html#length"><span class="id" title="definition">String.length</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#snd"><span class="id" title="definition">snd</span></a> (<a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#cur_output_line"><span class="id" title="projection">cur_output_line</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#pps:50"><span class="id" title="variable">pps</span></a>))<a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#pps:50"><span class="id" title="variable">pps</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="map_cur_output_line" class="idref" href="#map_cur_output_line"><span class="id" title="definition">map_cur_output_line</span></a> (<a id="f:51" class="idref" href="#f:51"><span class="id" title="binder">f</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac4"><span class="id" title="notation">*</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac4"><span class="id" title="notation">*</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) : <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#PrettyPrinter"><span class="id" title="definition">PrettyPrinter</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a> :=<br/>
<a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#map_pps"><span class="id" title="definition">map_pps</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#id"><span class="id" title="definition">id</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#id"><span class="id" title="definition">id</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#id"><span class="id" title="definition">id</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#f:51"><span class="id" title="variable">f</span></a>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="append" class="idref" href="#append"><span class="id" title="definition">append</span></a> (<a id="s:52" class="idref" href="#s:52"><span class="id" title="binder">s</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) : <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#PrettyPrinter"><span class="id" title="definition">PrettyPrinter</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a> :=<br/>
<a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#map_cur_output_line"><span class="id" title="definition">map_cur_output_line</span></a> (<span class="id" title="keyword">fun</span> '<a id="pat:55" class="idref" href="#pat:55"><span class="id" title="binder">(</span></a><a id="pat:55" class="idref" href="#pat:55"><span class="id" title="binder">n</span></a><a id="pat:55" class="idref" href="#pat:55"><span class="id" title="binder">,</span></a> <a id="pat:55" class="idref" href="#pat:55"><span class="id" title="binder">prev</span></a><a id="pat:55" class="idref" href="#pat:55"><span class="id" title="binder">)</span></a> => <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#n:54"><span class="id" title="variable">n</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#prev:53"><span class="id" title="variable">prev</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Strings.String.html#169ad156fbc6036a53a0338819a2b301"><span class="id" title="notation">++</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#s:52"><span class="id" title="variable">s</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a>).<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="append_nl" class="idref" href="#append_nl"><span class="id" title="definition">append_nl</span></a> : <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#PrettyPrinter"><span class="id" title="definition">PrettyPrinter</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a> :=<br/>
<span class="id" title="keyword">fun</span> <a id="pps:56" class="idref" href="#pps:56"><span class="id" title="binder">pps</span></a> =><br/>
<a class="idref" href="ConCert.Extraction.ResultMonad.html#Ok"><span class="id" title="constructor">Ok</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#tt"><span class="id" title="constructor">tt</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a><br/>
<a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">{|</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#indent_stack"><span class="id" title="projection">indent_stack</span></a> := <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#indent_stack"><span class="id" title="projection">indent_stack</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#pps:56"><span class="id" title="variable">pps</span></a>;<br/>
<a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#used_names"><span class="id" title="projection">used_names</span></a> := <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#used_names"><span class="id" title="projection">used_names</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#pps:56"><span class="id" title="variable">pps</span></a>;<br/>
<a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#output_lines"><span class="id" title="projection">output_lines</span></a> := <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#cur_output_line"><span class="id" title="projection">cur_output_line</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#pps:56"><span class="id" title="variable">pps</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#::list_scope:x_'::'_x"><span class="id" title="notation">::</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#output_lines"><span class="id" title="projection">output_lines</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#pps:56"><span class="id" title="variable">pps</span></a>;<br/>
<a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#cur_output_line"><span class="id" title="projection">cur_output_line</span></a> := <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#hd"><span class="id" title="definition">hd</span></a> 0 (<a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#indent_stack"><span class="id" title="projection">indent_stack</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#pps:56"><span class="id" title="variable">pps</span></a>)<a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> ""<a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">|})</span></a>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="monad_append_join" class="idref" href="#monad_append_join"><span class="id" title="definition">monad_append_join</span></a><br/>
(<a id="sep:57" class="idref" href="#sep:57"><span class="id" title="binder">sep</span></a> : <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#PrettyPrinter"><span class="id" title="definition">PrettyPrinter</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a>)<br/>
(<a id="xs:58" class="idref" href="#xs:58"><span class="id" title="binder">xs</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> (<a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#PrettyPrinter"><span class="id" title="definition">PrettyPrinter</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a>)) : <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#PrettyPrinter"><span class="id" title="definition">PrettyPrinter</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a> :=<br/>
<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.monad_utils.html#monad_fold_left"><span class="id" title="definition">monad_fold_left</span></a> (<span class="id" title="keyword">fun</span> <a id="sep':59" class="idref" href="#sep':59"><span class="id" title="binder">sep'</span></a> <a id="x:60" class="idref" href="#x:60"><span class="id" title="binder">x</span></a> => <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#sep':59"><span class="id" title="variable">sep'</span></a><a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.monad_utils.html#ad6f5869610c58e6b1cafcdf52bb7ae3"><span class="id" title="notation">;;</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#x:60"><span class="id" title="variable">x</span></a><a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.monad_utils.html#ad6f5869610c58e6b1cafcdf52bb7ae3"><span class="id" title="notation">;;</span></a> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.monad_utils.html#ret"><span class="id" title="method">ret</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#sep:57"><span class="id" title="variable">sep</span></a>) <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#xs:58"><span class="id" title="variable">xs</span></a> (<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.monad_utils.html#ret"><span class="id" title="method">ret</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#tt"><span class="id" title="constructor">tt</span></a>)<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.monad_utils.html#ad6f5869610c58e6b1cafcdf52bb7ae3"><span class="id" title="notation">;;</span></a><br/>
<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.monad_utils.html#ret"><span class="id" title="method">ret</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#tt"><span class="id" title="constructor">tt</span></a>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="append_join" class="idref" href="#append_join"><span class="id" title="definition">append_join</span></a> (<a id="sep:61" class="idref" href="#sep:61"><span class="id" title="binder">sep</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) (<a id="s:62" class="idref" href="#s:62"><span class="id" title="binder">s</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) : <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#PrettyPrinter"><span class="id" title="definition">PrettyPrinter</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a> :=<br/>
<a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#monad_append_join"><span class="id" title="definition">monad_append_join</span></a> (<a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#append"><span class="id" title="definition">append</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#sep:61"><span class="id" title="variable">sep</span></a>) (<a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#map"><span class="id" title="definition">map</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#append"><span class="id" title="definition">append</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#s:62"><span class="id" title="variable">s</span></a>).<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="monad_append_concat" class="idref" href="#monad_append_concat"><span class="id" title="definition">monad_append_concat</span></a> (<a id="xs:63" class="idref" href="#xs:63"><span class="id" title="binder">xs</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> (<a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#PrettyPrinter"><span class="id" title="definition">PrettyPrinter</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a>)) : <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#PrettyPrinter"><span class="id" title="definition">PrettyPrinter</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a> :=<br/>
<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.monad_utils.html#monad_map"><span class="id" title="definition">monad_map</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#id"><span class="id" title="definition">id</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#xs:63"><span class="id" title="variable">xs</span></a><a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.monad_utils.html#ad6f5869610c58e6b1cafcdf52bb7ae3"><span class="id" title="notation">;;</span></a><br/>
<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.monad_utils.html#ret"><span class="id" title="method">ret</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#tt"><span class="id" title="constructor">tt</span></a>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="append_concat" class="idref" href="#append_concat"><span class="id" title="definition">append_concat</span></a> (<a id="xs:64" class="idref" href="#xs:64"><span class="id" title="binder">xs</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) : <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#PrettyPrinter"><span class="id" title="definition">PrettyPrinter</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a> :=<br/>
<a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#monad_append_concat"><span class="id" title="definition">monad_append_concat</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#map"><span class="id" title="definition">map</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#append"><span class="id" title="definition">append</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#xs:64"><span class="id" title="variable">xs</span></a>).<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="fresh_name" class="idref" href="#fresh_name"><span class="id" title="definition">fresh_name</span></a> (<a id="name:65" class="idref" href="#name:65"><span class="id" title="binder">name</span></a> : <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Kernames.html#ident"><span class="id" title="definition">ident</span></a>) (<a id="extra_used:66" class="idref" href="#extra_used:66"><span class="id" title="binder">extra_used</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Kernames.html#ident"><span class="id" title="definition">ident</span></a>) : <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#PrettyPrinter"><span class="id" title="definition">PrettyPrinter</span></a> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Kernames.html#ident"><span class="id" title="definition">ident</span></a> :=<br/>
<a id="used:67" class="idref" href="#used:67"><span class="id" title="binder">used</span></a> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.monad_utils.html#6bec7af38cdf877f357faf8f1699c8f9"><span class="id" title="notation"><-</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#get_used_names"><span class="id" title="definition">get_used_names</span></a><a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.monad_utils.html#6bec7af38cdf877f357faf8f1699c8f9"><span class="id" title="notation">;;</span></a><br/>
<span class="id" title="keyword">let</span> <a id="used:68" class="idref" href="#used:68"><span class="id" title="binder">used</span></a> := (<a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#extra_used:66"><span class="id" title="variable">extra_used</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#bc347c51eaf667706ae54503b26d52c6"><span class="id" title="notation">++</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#used:67"><span class="id" title="variable">used</span></a>)%<span class="id" title="var">list</span> <span class="id" title="tactic">in</span><br/>
<span class="id" title="keyword">if</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#existsb"><span class="id" title="definition">existsb</span></a> (<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.utils.bytestring.html#String.eqb"><span class="id" title="definition">bytestring.String.eqb</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#name:65"><span class="id" title="variable">name</span></a>) <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#used:68"><span class="id" title="variable">used</span></a> <span class="id" title="keyword">then</span><br/>
(<span class="id" title="keyword">fix</span> <span class="id" title="var">f</span> <a id="n:69" class="idref" href="#n:69"><span class="id" title="binder">n</span></a> <a id="i:70" class="idref" href="#i:70"><span class="id" title="binder">i</span></a> :=<br/>
<span class="id" title="keyword">match</span> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#n:69"><span class="id" title="variable">n</span></a> <span class="id" title="keyword">with</span><br/>
| 0 => <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.monad_utils.html#ret"><span class="id" title="method">ret</span></a> (<a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#s_to_bs"><span class="id" title="abbreviation">s_to_bs</span></a> "unreachable")<br/>
| <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <span class="id" title="var">n</span> =><br/>
<span class="id" title="keyword">let</span> <a id="numbered_name:73" class="idref" href="#numbered_name:73"><span class="id" title="binder">numbered_name</span></a> := <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.utils.bytestring.html#String.append"><span class="id" title="definition">bytestring.String.append</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#name:65"><span class="id" title="variable">name</span></a> (<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.utils.MCString.html#string_of_nat"><span class="id" title="definition">MCString.string_of_nat</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#i:70"><span class="id" title="variable">i</span></a>) <span class="id" title="tactic">in</span><br/>
<span class="id" title="keyword">if</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#existsb"><span class="id" title="definition">existsb</span></a> (<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.utils.bytestring.html#String.eqb"><span class="id" title="definition">bytestring.String.eqb</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#numbered_name:73"><span class="id" title="variable">numbered_name</span></a>) <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#used:68"><span class="id" title="variable">used</span></a> <span class="id" title="keyword">then</span><br/>
<a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#f:71"><span class="id" title="variable">f</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#n:69"><span class="id" title="variable">n</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#i:70"><span class="id" title="variable">i</span></a>)<br/>
<span class="id" title="keyword">else</span><br/>
<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.monad_utils.html#ret"><span class="id" title="method">ret</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#numbered_name:73"><span class="id" title="variable">numbered_name</span></a><br/>
<span class="id" title="keyword">end</span>) (<a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#length"><span class="id" title="abbreviation">List.length</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#used:68"><span class="id" title="variable">used</span></a>)) 2<br/>
<span class="id" title="keyword">else</span><br/>
<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.monad_utils.html#ret"><span class="id" title="method">ret</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#name:65"><span class="id" title="variable">name</span></a>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="string_of_env_error" class="idref" href="#string_of_env_error"><span class="id" title="definition">string_of_env_error</span></a> <a id="0bb1b226b53b6455e93ad6a4d211d8ec" class="idref" href="#0bb1b226b53b6455e93ad6a4d211d8ec"><span class="id" title="binder">Σ</span></a> <a id="e:75" class="idref" href="#e:75"><span class="id" title="binder">e</span></a> :=<br/>
<span class="id" title="keyword">match</span> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#e:75"><span class="id" title="variable">e</span></a> <span class="id" title="keyword">with</span><br/>
| <a class="idref" href="https://metacoq.github.io/html/MetaCoq.SafeChecker.PCUICErrors.html#IllFormedDecl"><span class="id" title="constructor">IllFormedDecl</span></a> <span class="id" title="var">s</span> <span class="id" title="var">e</span> =><br/>
("IllFormedDecl " <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Strings.String.html#169ad156fbc6036a53a0338819a2b301"><span class="id" title="notation">++</span></a> <span class="id" title="var">s</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Strings.String.html#169ad156fbc6036a53a0338819a2b301"><span class="id" title="notation">++</span></a> "\nType error: " <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Strings.String.html#169ad156fbc6036a53a0338819a2b301"><span class="id" title="notation">++</span></a> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.SafeChecker.PCUICErrors.html#string_of_type_error"><span class="id" title="definition">string_of_type_error</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#0bb1b226b53b6455e93ad6a4d211d8ec"><span class="id" title="variable">Σ</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#e:75"><span class="id" title="variable">e</span></a>)%<span class="id" title="var">string</span><br/>
| <a class="idref" href="https://metacoq.github.io/html/MetaCoq.SafeChecker.PCUICErrors.html#AlreadyDeclared"><span class="id" title="constructor">AlreadyDeclared</span></a> <span class="id" title="var">s</span> => "Alreadydeclared " <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Strings.String.html#169ad156fbc6036a53a0338819a2b301"><span class="id" title="notation">++</span></a> <span class="id" title="var">s</span><br/>
<span class="id" title="keyword">end</span>%<span class="id" title="var">string</span>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="wrap_EnvCheck" class="idref" href="#wrap_EnvCheck"><span class="id" title="definition">wrap_EnvCheck</span></a> {<a id="astr:77" class="idref" href="#astr:77"><span class="id" title="binder">astr</span></a> <a id="A:78" class="idref" href="#A:78"><span class="id" title="binder">A</span></a>} <a id="f:79" class="idref" href="#f:79"><span class="id" title="binder">f</span></a> (<a id="ec:80" class="idref" href="#ec:80"><span class="id" title="binder">ec</span></a> : <a class="idref" href="https://metacoq.github.io/html/MetaCoq.SafeChecker.PCUICErrors.html#EnvCheck"><span class="id" title="inductive">EnvCheck</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#astr:77"><span class="id" title="variable">astr</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#A:78"><span class="id" title="variable">A</span></a>) : <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#PrettyPrinter"><span class="id" title="definition">PrettyPrinter</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#A:78"><span class="id" title="variable">A</span></a> :=<br/>
<span class="id" title="keyword">match</span> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#ec:80"><span class="id" title="variable">ec</span></a> <span class="id" title="keyword">with</span><br/>
| <a class="idref" href="https://metacoq.github.io/html/MetaCoq.SafeChecker.PCUICErrors.html#CorrectDecl"><span class="id" title="constructor">CorrectDecl</span></a> <span class="id" title="var">a</span> => <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.monad_utils.html#ret"><span class="id" title="method">ret</span></a> <span class="id" title="var">a</span><br/>
| <a class="idref" href="https://metacoq.github.io/html/MetaCoq.SafeChecker.PCUICErrors.html#EnvError"><span class="id" title="constructor">EnvError</span></a> <span class="id" title="var">Σ</span> <span class="id" title="var">err</span> =><br/>
<a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#printer_fail"><span class="id" title="definition">printer_fail</span></a> ("EnvError: " <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Strings.String.html#169ad156fbc6036a53a0338819a2b301"><span class="id" title="notation">++</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#string_of_env_error"><span class="id" title="definition">string_of_env_error</span></a> (<a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#f:79"><span class="id" title="variable">f</span></a> <span class="id" title="var">Σ</span>) <span class="id" title="var">err</span>)<br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<span class="id" title="keyword">Module</span> <a id="P" class="idref" href="#P"><span class="id" title="module">P</span></a> := <a class="idref" href="https://metacoq.github.io/html/MetaCoq.PCUIC.PCUICAst.html#"><span class="id" title="module">PCUICAst</span></a>.<br/>
<span class="id" title="keyword">Definition</span> <a id="wrap_typing_result" class="idref" href="#wrap_typing_result"><span class="id" title="definition">wrap_typing_result</span></a> {<a id="A:82" class="idref" href="#A:82"><span class="id" title="binder">A</span></a>} (<a id="af0c8f8f5ce7afdccb859d2482b046b5" class="idref" href="#af0c8f8f5ce7afdccb859d2482b046b5"><span class="id" title="binder">Σ</span></a> : <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#global_env"><span class="id" title="record">P.PCUICEnvironment.global_env</span></a>) (<a id="tr:84" class="idref" href="#tr:84"><span class="id" title="binder">tr</span></a> : <a class="idref" href="https://metacoq.github.io/html/MetaCoq.SafeChecker.PCUICErrors.html#typing_result"><span class="id" title="inductive">typing_result</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#A:82"><span class="id" title="variable">A</span></a>) : <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#PrettyPrinter"><span class="id" title="definition">PrettyPrinter</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#A:82"><span class="id" title="variable">A</span></a> :=<br/>
<span class="id" title="keyword">match</span> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#tr:84"><span class="id" title="variable">tr</span></a> <span class="id" title="keyword">with</span><br/>
| <a class="idref" href="https://metacoq.github.io/html/MetaCoq.SafeChecker.PCUICErrors.html#Checked"><span class="id" title="constructor">Checked</span></a> <span class="id" title="var">et</span> => <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.monad_utils.html#ret"><span class="id" title="method">ret</span></a> <span class="id" title="var">et</span><br/>
| <a class="idref" href="https://metacoq.github.io/html/MetaCoq.SafeChecker.PCUICErrors.html#TypeError"><span class="id" title="constructor">TypeError</span></a> <span class="id" title="var">te</span> =><br/>
<a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#printer_fail"><span class="id" title="definition">printer_fail</span></a> ("TypeError: " <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Strings.String.html#169ad156fbc6036a53a0338819a2b301"><span class="id" title="notation">++</span></a> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.SafeChecker.PCUICErrors.html#string_of_type_error"><span class="id" title="definition">string_of_type_error</span></a> (<a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#empty_ext"><span class="id" title="definition">P.PCUICEnvironment.empty_ext</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#af0c8f8f5ce7afdccb859d2482b046b5"><span class="id" title="variable">Σ</span></a>) <span class="id" title="var">te</span>)<br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="wrap_option" class="idref" href="#wrap_option"><span class="id" title="definition">wrap_option</span></a> {<a id="A:86" class="idref" href="#A:86"><span class="id" title="binder">A</span></a>} (<a id="o:87" class="idref" href="#o:87"><span class="id" title="binder">o</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#A:86"><span class="id" title="variable">A</span></a>) (<a id="err:88" class="idref" href="#err:88"><span class="id" title="binder">err</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) : <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#PrettyPrinter"><span class="id" title="definition">PrettyPrinter</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#A:86"><span class="id" title="variable">A</span></a> :=<br/>
<span class="id" title="keyword">match</span> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#o:87"><span class="id" title="variable">o</span></a> <span class="id" title="keyword">with</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">a</span> => <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.monad_utils.html#ret"><span class="id" title="method">ret</span></a> <span class="id" title="var">a</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a> => <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#printer_fail"><span class="id" title="definition">printer_fail</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#err:88"><span class="id" title="variable">err</span></a><br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="wrap_result" class="idref" href="#wrap_result"><span class="id" title="definition">wrap_result</span></a> {<a id="T:90" class="idref" href="#T:90"><span class="id" title="binder">T</span></a> <a id="E:91" class="idref" href="#E:91"><span class="id" title="binder">E</span></a>} (<a id="r:92" class="idref" href="#r:92"><span class="id" title="binder">r</span></a> : <a class="idref" href="ConCert.Extraction.ResultMonad.html#result"><span class="id" title="inductive">result</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#T:90"><span class="id" title="variable">T</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#E:91"><span class="id" title="variable">E</span></a>) (<a id="err_string:93" class="idref" href="#err_string:93"><span class="id" title="binder">err_string</span></a> : <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#E:91"><span class="id" title="variable">E</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) : <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#PrettyPrinter"><span class="id" title="definition">PrettyPrinter</span></a> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#T:90"><span class="id" title="variable">T</span></a> :=<br/>
<span class="id" title="keyword">match</span> <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#r:92"><span class="id" title="variable">r</span></a> <span class="id" title="keyword">with</span><br/>
| <a class="idref" href="ConCert.Extraction.ResultMonad.html#Ok"><span class="id" title="constructor">Ok</span></a> <span class="id" title="var">t</span> => <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.monad_utils.html#ret"><span class="id" title="method">ret</span></a> <span class="id" title="var">t</span><br/>
| <a class="idref" href="ConCert.Extraction.ResultMonad.html#Err"><span class="id" title="constructor">Err</span></a> <span class="id" title="var">e</span> => <a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#printer_fail"><span class="id" title="definition">printer_fail</span></a> (<a class="idref" href="ConCert.Extraction.PrettyPrinterMonad.html#err_string:93"><span class="id" title="variable">err_string</span></a> <span class="id" title="var">e</span>)<br/>
<span class="id" title="keyword">end</span>.<br/>
</div>
</div>
<div id="footer">
Generated by <a href="https://coq.inria.fr/">coqdoc</a> and improved with <a href="https://github.com/tebbi/coqdocjs">CoqdocJS</a> and <a href="https://github.com/jgallen23/toc">TOC</a>
</div>
</div>
<script>
const elements = document.getElementsByClassName("libtitle");
while(elements.length > 0){
elements[0].parentNode.removeChild(elements[0]);
}
if (window.location.pathname.endsWith("/toc.html")) {
const jstocDiv = document.getElementById("js-toc");
jstocDiv.classList.remove("toc");
jstocDiv.classList.add("jstoc-hidden");
const jstocHeaderDiv = document.getElementById("js-toc-header");
jstocHeaderDiv.classList.add("jstoc-hidden");
const mainDiv = document.getElementById("main");
mainDiv.classList.add("jstoc-hidden-main");
const toggleDiv = document.getElementById("toggle-toc");
toggleDiv.classList.add("jstoc-hidden");
}
console.log(window.location.pathname);
</script>
<script type="text/javascript" src="toc.js"></script>
</body>
</html>
