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.CertifyingInlining.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.CertifyingInlining</h1>
<div class="code">
</div>
<div class="doc">
<a id="lab6"></a><h1 class="section">Inlining pass on the Template Coq representation</h1>
<div class="paragraph"> </div>
Essentially, just an adaptaion of the inlining pass on the erased representation.
After the pass is applied we generate proofs that the original and the transformed terms are equal in the theory of Coq. The proofs are just by <span class="inlinecode"><a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Logic.html#eq_refl"><span class="id" title="constructor">eq_refl</span></a></span>, since the terms are convertible
</div>
<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.String.html#"><span class="id" title="library">String</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.Bool.Bool.html#"><span class="id" title="library">Bool</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.Transform.html#"><span class="id" title="library">Transform</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/>
<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.CertifyingBeta.html#"><span class="id" title="library">CertifyingBeta</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.Utils.html#"><span class="id" title="library">Utils</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.Certifying.html#"><span class="id" title="library">Certifying</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.All.html#"><span class="id" title="library">All</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.Kernames.html#"><span class="id" title="library">Kernames</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">MCMonadNotation</span></a>.<br/>
<br/>
<span class="id" title="keyword">Section</span> <a id="inlining" class="idref" href="#inlining"><span class="id" title="section">inlining</span></a>.<br/>
<span class="id" title="keyword">Context</span> (<a id="should_inline:1" class="idref" href="#should_inline:1"><span class="id" title="binder">should_inline</span></a> : <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Kernames.html#kername"><span class="id" title="definition">kername</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#bool"><span class="id" title="inductive">bool</span></a>).<br/>
<span class="id" title="keyword">Context</span> <a class="idref" href="ConCert.Extraction.Common.html#to_kername"><span class="id" title="definition">(</span></a><a id="ebf069dbc779b42a15c441a6d39d5f83" class="idref" href="#ebf069dbc779b42a15c441a6d39d5f83"><span class="id" title="binder">Σ</span></a> : <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.global_env"><span class="id" title="record">global_env</span></a>).<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="inline_const" class="idref" href="#inline_const"><span class="id" title="definition">inline_const</span></a> (<a id="kn:3" class="idref" href="#kn:3"><span class="id" title="binder">kn</span></a> : <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Kernames.html#kername"><span class="id" title="definition">kername</span></a>) (<a id="u:4" class="idref" href="#u:4"><span class="id" title="binder">u</span></a> : <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Universes.html#Instance.t"><span class="id" title="definition">Instance.t</span></a>) (<a id="args:5" class="idref" href="#args:5"><span class="id" title="binder">args</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.Ast.html#term"><span class="id" title="inductive">term</span></a>) : <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#term"><span class="id" title="inductive">term</span></a> :=<br/>
<span class="id" title="keyword">let</span> <a id="const:6" class="idref" href="#const:6"><span class="id" title="binder">const</span></a> := <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#tConst"><span class="id" title="constructor">tConst</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#kn:3"><span class="id" title="variable">kn</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#u:4"><span class="id" title="variable">u</span></a> <span class="id" title="tactic">in</span><br/>
<span class="id" title="keyword">match</span> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.lookup_env"><span class="id" title="definition">lookup_env</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#1b0fae7f9b6290849ff7c3ac38c2ca0b"><span class="id" title="variable">Σ</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#kn:3"><span class="id" title="variable">kn</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> (<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.ConstantDecl"><span class="id" title="constructor">ConstantDecl</span></a> <span class="id" title="var">cst</span>) =><br/>
<span class="id" title="keyword">match</span> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.cst_body"><span class="id" title="projection">cst_body</span></a> <span class="id" title="var">cst</span> <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">body</span> <span class="comment">(* once told me *)</span> =><br/>
<span class="comment">(* Often the first beta will expose an iota (record projection),<br/>
and the projected field is often a function, so we do another beta *)</span><br/>
<span class="id" title="keyword">let</span> (<a id="hd:7" class="idref" href="#hd:7"><span class="id" title="binder">hd</span></a>, <a id="args:8" class="idref" href="#args:8"><span class="id" title="binder">args</span></a>) := <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.AstUtils.html#decompose_app"><span class="id" title="definition">decompose_app</span></a> (<a class="idref" href="ConCert.Extraction.Common.html#beta_body"><span class="id" title="definition">beta_body</span></a> <span class="id" title="var">body</span> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#args:5"><span class="id" title="variable">args</span></a>) <span class="id" title="tactic">in</span><br/>
<a class="idref" href="ConCert.Extraction.Common.html#beta_body"><span class="id" title="definition">beta_body</span></a> (<a class="idref" href="ConCert.Extraction.Common.html#iota_body"><span class="id" title="definition">iota_body</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#1b0fae7f9b6290849ff7c3ac38c2ca0b"><span class="id" title="variable">Σ</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#hd:7"><span class="id" title="variable">hd</span></a>) <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#args:8"><span class="id" title="variable">args</span></a><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="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#tApp"><span class="id" title="constructor">tApp</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#const:6"><span class="id" title="variable">const</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#args:5"><span class="id" title="variable">args</span></a><br/>
<span class="id" title="keyword">end</span><br/>
| <span class="id" title="var">_</span> => <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#tApp"><span class="id" title="constructor">tApp</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#const:6"><span class="id" title="variable">const</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#args:5"><span class="id" title="variable">args</span></a><br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<span class="id" title="keyword">Fixpoint</span> <a id="inline_aux" class="idref" href="#inline_aux"><span class="id" title="definition">inline_aux</span></a> (<a id="args:9" class="idref" href="#args:9"><span class="id" title="binder">args</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.Ast.html#term"><span class="id" title="inductive">term</span></a>) (<a id="t:10" class="idref" href="#t:10"><span class="id" title="binder">t</span></a> : <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#term"><span class="id" title="inductive">term</span></a>) : <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#term"><span class="id" title="inductive">term</span></a> :=<br/>
<span class="id" title="keyword">match</span> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#t:10"><span class="id" title="variable">t</span></a> <span class="id" title="keyword">with</span><br/>
| <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#tApp"><span class="id" title="constructor">tApp</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> <span class="id" title="var">args0</span> => <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#inline_aux:11"><span class="id" title="definition">inline_aux</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.CertifyingInlining.html#inline_aux:11"><span class="id" title="definition">inline_aux</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>) <span class="id" title="var">args0</span> <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.CertifyingInlining.html#args:9"><span class="id" title="variable">args</span></a>) <span class="id" title="var">hd</span><br/>
| <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#tCast"><span class="id" title="constructor">tCast</span></a> <span class="id" title="var">t0</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> =><br/>
<span class="comment">(* NOTE: removing casts leads to producing more definitions at the proof<br/>
generation phase, even for the cases when there isn't anything to<br/>
inline, because the structure of the term has changed.<br/>
We cannot determine at this point whether we should inline something or<br/>
nothing at all, since <span class="inlinecode"><span class="id" title="var">should_inline</span></span> is a function *)</span><br/>
<a class="idref" href="ConCert.Extraction.CertifyingInlining.html#inline_aux:11"><span class="id" title="definition">inline_aux</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#args:9"><span class="id" title="variable">args</span></a> <span class="id" title="var">t0</span><br/>
| <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#tConst"><span class="id" title="constructor">tConst</span></a> <span class="id" title="var">kn</span> <span class="id" title="var">u</span> =><br/>
<span class="id" title="keyword">if</span> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#inlining.should_inline"><span class="id" title="variable">should_inline</span></a> <span class="id" title="var">kn</span> <span class="id" title="keyword">then</span><br/>
<span class="id" title="keyword">match</span> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.lookup_env"><span class="id" title="definition">lookup_env</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#1b0fae7f9b6290849ff7c3ac38c2ca0b"><span class="id" title="variable">Σ</span></a> <span class="id" title="var">kn</span> <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> (<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.ConstantDecl"><span class="id" title="constructor">ConstantDecl</span></a> <span class="id" title="var">cst</span>) =><br/>
<span class="id" title="keyword">match</span> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.cst_body"><span class="id" title="projection">cst_body</span></a> <span class="id" title="var">cst</span> <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">body</span> =><br/>
<span class="id" title="keyword">let</span> (<a id="hd:13" class="idref" href="#hd:13"><span class="id" title="binder">hd</span></a>, <a id="args:14" class="idref" href="#args:14"><span class="id" title="binder">args</span></a>) := <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.AstUtils.html#decompose_app"><span class="id" title="definition">decompose_app</span></a> (<a class="idref" href="ConCert.Extraction.Common.html#beta_body"><span class="id" title="definition">beta_body</span></a> <span class="id" title="var">body</span> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#args:9"><span class="id" title="variable">args</span></a>) <span class="id" title="tactic">in</span><br/>
<span class="comment">(* NOTE: Often the first beta will expose an iota (record projection),<br/>
and the projected field is often a function, so we do another beta *)</span><br/>
<span class="id" title="keyword">let</span> <a id="res:15" class="idref" href="#res:15"><span class="id" title="binder">res</span></a> := <a class="idref" href="ConCert.Extraction.Common.html#beta_body"><span class="id" title="definition">beta_body</span></a> (<a class="idref" href="ConCert.Extraction.Common.html#iota_body"><span class="id" title="definition">iota_body</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#1b0fae7f9b6290849ff7c3ac38c2ca0b"><span class="id" title="variable">Σ</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#hd:13"><span class="id" title="variable">hd</span></a>) <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#args:14"><span class="id" title="variable">args</span></a> <span class="id" title="tactic">in</span><br/>
<span class="comment">(* NOTE: after we beta-reduced the function coming from projection,<br/>
it might intorduce new redexes. This is often the case when using<br/>
option monads. Therefore, we do a pass that find the redexes and<br/>
beta-reduces them further. *)</span><br/>
<a class="idref" href="ConCert.Extraction.CertifyingBeta.html#betared"><span class="id" title="definition">betared</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#res:15"><span class="id" title="variable">res</span></a><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="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#mkApps"><span class="id" title="definition">mkApps</span></a> (<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#tConst"><span class="id" title="constructor">tConst</span></a> <span class="id" title="var">kn</span> <span class="id" title="var">u</span>) <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#args:9"><span class="id" title="variable">args</span></a><br/>
<span class="id" title="keyword">end</span><br/>
| <span class="id" title="var">_</span> => <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#mkApps"><span class="id" title="definition">mkApps</span></a> (<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#tConst"><span class="id" title="constructor">tConst</span></a> <span class="id" title="var">kn</span> <span class="id" title="var">u</span>) <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#args:9"><span class="id" title="variable">args</span></a><br/>
<span class="id" title="keyword">end</span><br/>
<span class="id" title="keyword">else</span><br/>
<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#mkApps"><span class="id" title="definition">mkApps</span></a> (<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#tConst"><span class="id" title="constructor">tConst</span></a> <span class="id" title="var">kn</span> <span class="id" title="var">u</span>) <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#args:9"><span class="id" title="variable">args</span></a><br/>
| <span class="id" title="var">t</span> => <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#mkApps"><span class="id" title="definition">mkApps</span></a> (<a class="idref" href="ConCert.Extraction.Common.html#map_subterms"><span class="id" title="definition">map_subterms</span></a> (<a class="idref" href="ConCert.Extraction.CertifyingInlining.html#inline_aux:11"><span class="id" title="definition">inline_aux</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>) <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#t:10"><span class="id" title="variable">t</span></a>) <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#args:9"><span class="id" title="variable">args</span></a><br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="inline" class="idref" href="#inline"><span class="id" title="definition">inline</span></a> : <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#term"><span class="id" title="inductive">term</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="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#term"><span class="id" title="inductive">term</span></a> := <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#inline_aux"><span class="id" title="definition">inline_aux</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/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="inline_in_constant_body" class="idref" href="#inline_in_constant_body"><span class="id" title="definition">inline_in_constant_body</span></a> <a id="cst:16" class="idref" href="#cst:16"><span class="id" title="binder">cst</span></a> :=<br/>
{| <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.cst_type"><span class="id" title="projection">cst_type</span></a> := <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#inline"><span class="id" title="definition">inline</span></a> (<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.cst_type"><span class="id" title="projection">cst_type</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#cst:16"><span class="id" title="variable">cst</span></a>);<br/>
<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.cst_universes"><span class="id" title="projection">cst_universes</span></a> := <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.cst_universes"><span class="id" title="projection">cst_universes</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#cst:16"><span class="id" title="variable">cst</span></a>;<br/>
<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.cst_body"><span class="id" title="projection">cst_body</span></a> := <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#option_map"><span class="id" title="definition">option_map</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#inline"><span class="id" title="definition">inline</span></a> (<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.cst_body"><span class="id" title="projection">cst_body</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#cst:16"><span class="id" title="variable">cst</span></a>);<br/>
<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.cst_relevance"><span class="id" title="projection">cst_relevance</span></a> := <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#cst:16"><span class="id" title="variable">cst</span></a>.(<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.cst_relevance"><span class="id" title="projection">cst_relevance</span></a>) |}.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="inline_oib" class="idref" href="#inline_oib"><span class="id" title="definition">inline_oib</span></a> (<a id="npars:17" class="idref" href="#npars:17"><span class="id" title="binder">npars</span></a> <a id="arities:18" class="idref" href="#arities:18"><span class="id" title="binder">arities</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 id="oib:19" class="idref" href="#oib:19"><span class="id" title="binder">oib</span></a> : <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.one_inductive_body"><span class="id" title="record">one_inductive_body</span></a>) :=<br/>
{| <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.ind_name"><span class="id" title="projection">ind_name</span></a> := <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#oib:19"><span class="id" title="variable">oib</span></a>.(<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.ind_name"><span class="id" title="projection">ind_name</span></a>);<br/>
<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.ind_indices"><span class="id" title="projection">ind_indices</span></a> := <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#oib:19"><span class="id" title="variable">oib</span></a>.(<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.ind_indices"><span class="id" title="projection">ind_indices</span></a>);<br/>
<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.ind_sort"><span class="id" title="projection">ind_sort</span></a> := <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#oib:19"><span class="id" title="variable">oib</span></a>.(<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.ind_sort"><span class="id" title="projection">ind_sort</span></a>);<br/>
<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.ind_type"><span class="id" title="projection">ind_type</span></a> := <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#inline"><span class="id" title="definition">inline</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#oib:19"><span class="id" title="variable">oib</span></a>.(<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.ind_type"><span class="id" title="projection">ind_type</span></a>);<br/>
<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.ind_kelim"><span class="id" title="projection">ind_kelim</span></a> := <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#oib:19"><span class="id" title="variable">oib</span></a>.(<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.ind_kelim"><span class="id" title="projection">ind_kelim</span></a>);<br/>
<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.ind_ctors"><span class="id" title="projection">ind_ctors</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="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.map_constructor_body"><span class="id" title="definition">map_constructor_body</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#npars:17"><span class="id" title="variable">npars</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#arities:18"><span class="id" title="variable">arities</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">_</span> => <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#inline"><span class="id" title="definition">inline</span></a> )) <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#oib:19"><span class="id" title="variable">oib</span></a>.(<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.ind_ctors"><span class="id" title="projection">ind_ctors</span></a>);<br/>
<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.ind_projs"><span class="id" title="projection">ind_projs</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> (<span class="id" title="keyword">fun</span> '(<a id="pat:23" class="idref" href="#pat:23"><span class="id" title="binder">Build_projection_body</span></a> <a id="pat:23" class="idref" href="#pat:23"><span class="id" title="binder">p_nm</span></a> <a id="pat:23" class="idref" href="#pat:23"><span class="id" title="binder">p_rel</span></a> <a id="pat:23" class="idref" href="#pat:23"><span class="id" title="binder">p_ty</span></a>) =><br/>
<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.Build_projection_body"><span class="id" title="constructor">Build_projection_body</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#p_nm:22"><span class="id" title="variable">p_nm</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#p_rel:21"><span class="id" title="variable">p_rel</span></a> (<a class="idref" href="ConCert.Extraction.CertifyingInlining.html#inline"><span class="id" title="definition">inline</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#p_ty:20"><span class="id" title="variable">p_ty</span></a>)) <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#oib:19"><span class="id" title="variable">oib</span></a>.(<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.ind_projs"><span class="id" title="projection">ind_projs</span></a>);<br/>
<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.ind_relevance"><span class="id" title="projection">ind_relevance</span></a> := <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#oib:19"><span class="id" title="variable">oib</span></a>.(<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.ind_relevance"><span class="id" title="projection">ind_relevance</span></a>) |}.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="inline_context_decl" class="idref" href="#inline_context_decl"><span class="id" title="definition">inline_context_decl</span></a> (<a id="cd:24" class="idref" href="#cd:24"><span class="id" title="binder">cd</span></a> : <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.context_decl"><span class="id" title="abbreviation">context_decl</span></a>) : <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.context_decl"><span class="id" title="abbreviation">context_decl</span></a> :=<br/>
{| <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.BasicAst.html#decl_name"><span class="id" title="projection">decl_name</span></a> := <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#cd:24"><span class="id" title="variable">cd</span></a>.(<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.BasicAst.html#decl_name"><span class="id" title="projection">decl_name</span></a>);<br/>
<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.BasicAst.html#decl_body"><span class="id" title="projection">decl_body</span></a> := <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#option_map"><span class="id" title="definition">option_map</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#inline"><span class="id" title="definition">inline</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#cd:24"><span class="id" title="variable">cd</span></a>.(<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.BasicAst.html#decl_body"><span class="id" title="projection">decl_body</span></a>);<br/>
<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.BasicAst.html#decl_type"><span class="id" title="projection">decl_type</span></a> := <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#cd:24"><span class="id" title="variable">cd</span></a>.(<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.BasicAst.html#decl_type"><span class="id" title="projection">decl_type</span></a>) |}.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="inline_in_decl" class="idref" href="#inline_in_decl"><span class="id" title="definition">inline_in_decl</span></a> <a id="d:25" class="idref" href="#d:25"><span class="id" title="binder">d</span></a> :=<br/>
<span class="id" title="keyword">match</span> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#d:25"><span class="id" title="variable">d</span></a> <span class="id" title="keyword">with</span><br/>
| <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.ConstantDecl"><span class="id" title="constructor">ConstantDecl</span></a> <span class="id" title="var">cst</span> => <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.ConstantDecl"><span class="id" title="constructor">ConstantDecl</span></a> (<a class="idref" href="ConCert.Extraction.CertifyingInlining.html#inline_in_constant_body"><span class="id" title="definition">inline_in_constant_body</span></a> <span class="id" title="var">cst</span>)<br/>
| <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.InductiveDecl"><span class="id" title="constructor">InductiveDecl</span></a> <span class="id" title="var">mib</span> =><br/>
<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.InductiveDecl"><span class="id" title="constructor">InductiveDecl</span></a><br/>
{| <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.ind_finite"><span class="id" title="projection">ind_finite</span></a> := <span class="id" title="var">mib</span>.(<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.ind_finite"><span class="id" title="projection">ind_finite</span></a>);<br/>
<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.ind_npars"><span class="id" title="projection">ind_npars</span></a> := <span class="id" title="var">mib</span>.(<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.ind_npars"><span class="id" title="projection">ind_npars</span></a>);<br/>
<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.ind_params"><span class="id" title="projection">ind_params</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.CertifyingInlining.html#inline_context_decl"><span class="id" title="definition">inline_context_decl</span></a> <span class="id" title="var">mib</span>.(<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.ind_params"><span class="id" title="projection">ind_params</span></a>);<br/>
<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.ind_bodies"><span class="id" title="projection">ind_bodies</span></a> :=<br/>
<span class="id" title="keyword">let</span> <a id="arities:27" class="idref" href="#arities:27"><span class="id" title="binder">arities</span></a> := <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.utils.MCList.html#50abc9bd1bb81dce67ffb7e42f8ed4c9"><span class="id" title="notation">#|</span></a><a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.arities_context"><span class="id" title="definition">arities_context</span></a> <span class="id" title="var">mib</span>.(<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.ind_bodies"><span class="id" title="projection">ind_bodies</span></a>)<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.utils.MCList.html#50abc9bd1bb81dce67ffb7e42f8ed4c9"><span class="id" title="notation">|</span></a> <span class="id" title="tactic">in</span><br/>
<span class="id" title="keyword">let</span> <a id="npars:28" class="idref" href="#npars:28"><span class="id" title="binder">npars</span></a> := (<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.context_assumptions"><span class="id" title="definition">context_assumptions</span></a> <span class="id" title="var">mib</span>.(<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.ind_params"><span class="id" title="projection">ind_params</span></a>)) <span class="id" title="tactic">in</span><br/>
<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.CertifyingInlining.html#inline_oib"><span class="id" title="definition">inline_oib</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#npars:28"><span class="id" title="variable">npars</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#arities:27"><span class="id" title="variable">arities</span></a>) <span class="id" title="var">mib</span>.(<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.ind_bodies"><span class="id" title="projection">ind_bodies</span></a>);<br/>
<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.ind_universes"><span class="id" title="projection">ind_universes</span></a> := <span class="id" title="var">mib</span>.(<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.ind_universes"><span class="id" title="projection">ind_universes</span></a>);<br/>
<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.ind_variance"><span class="id" title="projection">ind_variance</span></a> := <span class="id" title="var">mib</span>.(<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.ind_variance"><span class="id" title="projection">ind_variance</span></a>) |}<br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#inlining"><span class="id" title="section">inlining</span></a>.<br/>
<br/>
<span class="comment">(* Definition inline_in_decls (should_inline : kername -> bool) (Σ : global_declarations) : global_env:= *)</span><br/>
<span class="comment">(* let newΣ := *)</span><br/>
<span class="comment">(* fold_right (fun '(kn, decl) decls => *)</span><br/>
<span class="comment">(* let Σ0 := {| universes := Σ.(universes); *)</span><br/>
<span class="comment">(* declarations := decls |} in *)</span><br/>
<span class="comment">(* (kn, inline_in_decl should_inline Σ0 decl) :: decls) <span class="inlinecode"></span>) Σ in *)</span><br/>
<span class="comment">(* map_global_env_decls (filter (fun '(kn, _) => negb (should_inline kn))) newΣ. *)</span><br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="inline_globals" class="idref" href="#inline_globals"><span class="id" title="definition">inline_globals</span></a> (<a id="should_inline:29" class="idref" href="#should_inline:29"><span class="id" title="binder">should_inline</span></a> : <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Kernames.html#kername"><span class="id" title="definition">kername</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#bool"><span class="id" title="inductive">bool</span></a>) (<a id="837da4610b9e0a7574f49c54d2569297" class="idref" href="#837da4610b9e0a7574f49c54d2569297"><span class="id" title="binder">Σ</span></a> : <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.global_declarations"><span class="id" title="definition">global_declarations</span></a>) : <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.global_declarations"><span class="id" title="definition">global_declarations</span></a> :=<br/>
<span class="id" title="keyword">let</span> <a id="5c8e3ce20599423577456d54bd161afe" class="idref" href="#5c8e3ce20599423577456d54bd161afe"><span class="id" title="binder">newΣ</span></a> :=<br/>
<a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#fold_right"><span class="id" title="definition">fold_right</span></a> (<span class="id" title="keyword">fun</span> '<a id="pat:33" class="idref" href="#pat:33"><span class="id" title="binder">(</span></a><a id="pat:33" class="idref" href="#pat:33"><span class="id" title="binder">kn</span></a><a id="pat:33" class="idref" href="#pat:33"><span class="id" title="binder">,</span></a> <a id="pat:33" class="idref" href="#pat:33"><span class="id" title="binder">decl</span></a><a id="pat:33" class="idref" href="#pat:33"><span class="id" title="binder">)</span></a> <a id="decls:34" class="idref" href="#decls:34"><span class="id" title="binder">decls</span></a> =><br/>
<span class="comment">(* Universes play no role in inlining, but carrying<br/>
universes is expensive if the set is big. However, all<br/>
the lookup functions take <span class="inlinecode"><span class="id" title="var">global_env</span></span>. *)</span><br/>
<span class="id" title="keyword">let</span> <a id="0e91550d34bcb07655b3e35516da888d" class="idref" href="#0e91550d34bcb07655b3e35516da888d"><span class="id" title="binder">Σ0</span></a> := {| <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.universes"><span class="id" title="projection">universes</span></a> := <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Universes.html#ContextSet.empty"><span class="id" title="definition">ContextSet.empty</span></a>;<br/>
<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.declarations"><span class="id" title="projection">declarations</span></a> := <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#decls:34"><span class="id" title="variable">decls</span></a> |} <span class="id" title="tactic">in</span><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.CertifyingInlining.html#kn:32"><span class="id" title="variable">kn</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.CertifyingInlining.html#inline_in_decl"><span class="id" title="definition">inline_in_decl</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#should_inline:29"><span class="id" title="variable">should_inline</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#0e91550d34bcb07655b3e35516da888d"><span class="id" title="variable">Σ0</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#decl:31"><span class="id" title="variable">decl</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#::list_scope:x_'::'_x"><span class="id" title="notation">::</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#decls:34"><span class="id" title="variable">decls</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> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#837da4610b9e0a7574f49c54d2569297"><span class="id" title="variable">Σ</span></a> <span class="id" title="tactic">in</span><br/>
<a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Lists.List.html#filter"><span class="id" title="definition">filter</span></a> (<span class="id" title="keyword">fun</span> '<a id="pat:38" class="idref" href="#pat:38"><span class="id" title="binder">(</span></a><a id="pat:38" class="idref" href="#pat:38"><span class="id" title="binder">kn</span></a><a id="pat:38" class="idref" href="#pat:38"><span class="id" title="binder">,</span></a> <a id="pat:38" class="idref" href="#pat:38"><span class="id" title="binder">_</span></a><a id="pat:38" class="idref" href="#pat:38"><span class="id" title="binder">)</span></a> => <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#negb"><span class="id" title="definition">negb</span></a> (<a class="idref" href="ConCert.Extraction.CertifyingInlining.html#should_inline:29"><span class="id" title="variable">should_inline</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#kn:37"><span class="id" title="variable">kn</span></a>)) <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#5c8e3ce20599423577456d54bd161afe"><span class="id" title="variable">newΣ</span></a>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="inline_globals_template" class="idref" href="#inline_globals_template"><span class="id" title="definition">inline_globals_template</span></a><br/>
(<a id="mpath:39" class="idref" href="#mpath:39"><span class="id" title="binder">mpath</span></a> : <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Kernames.html#modpath"><span class="id" title="inductive">modpath</span></a>)<br/>
(<a id="a5fa9249bdc19684169f7ebb302b006b" class="idref" href="#a5fa9249bdc19684169f7ebb302b006b"><span class="id" title="binder">Σ</span></a> : <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.global_declarations"><span class="id" title="definition">global_declarations</span></a>)<br/>
(<a id="should_inline:41" class="idref" href="#should_inline:41"><span class="id" title="binder">should_inline</span></a> : <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Kernames.html#kername"><span class="id" title="definition">kername</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#bool"><span class="id" title="inductive">bool</span></a>)<br/>
(<a id="seeds:42" class="idref" href="#seeds:42"><span class="id" title="binder">seeds</span></a> : <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Kernames.html#KernameSet.t"><span class="id" title="definition">KernameSet.t</span></a>)<br/>
: <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.TemplateMonad.Core.html#TemplateMonad"><span class="id" title="inductive">TemplateMonad</span></a> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.global_declarations"><span class="id" title="definition">global_declarations</span></a> :=<br/>
<span class="id" title="keyword">let</span> <a id="suffix:43" class="idref" href="#suffix:43"><span class="id" title="binder">suffix</span></a> := "_after_inlining" <span class="id" title="tactic">in</span><br/>
<a id="decls_inlined:44" class="idref" href="#decls_inlined:44"><span class="id" title="binder">decls_inlined</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="https://metacoq.github.io/html/MetaCoq.Template.TemplateMonad.Core.html#tmEval"><span class="id" title="constructor">tmEval</span></a> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.TemplateMonad.Common.html#lazy"><span class="id" title="constructor">lazy</span></a> (<a class="idref" href="ConCert.Extraction.CertifyingInlining.html#inline_globals"><span class="id" title="definition">inline_globals</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#should_inline:41"><span class="id" title="variable">should_inline</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#a5fa9249bdc19684169f7ebb302b006b"><span class="id" title="variable">Σ</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/>
<a class="idref" href="ConCert.Extraction.Certifying.html#gen_defs_and_proofs"><span class="id" title="definition">gen_defs_and_proofs</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#a5fa9249bdc19684169f7ebb302b006b"><span class="id" title="variable">Σ</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#decls_inlined:44"><span class="id" title="variable">decls_inlined</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#mpath:39"><span class="id" title="variable">mpath</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#suffix:43"><span class="id" title="variable">suffix</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#seeds:42"><span class="id" title="variable">seeds</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="ConCert.Extraction.CertifyingInlining.html#decls_inlined:44"><span class="id" title="variable">decls_inlined</span></a>.<br/>
<br/>
<span class="comment">(* Mainly for testing purposes *)</span><br/>
<span class="id" title="keyword">Definition</span> <a id="inline_def" class="idref" href="#inline_def"><span class="id" title="definition">inline_def</span></a> {<a id="A:45" class="idref" href="#A:45"><span class="id" title="binder">A</span></a>}<br/>
(<a id="should_inline:46" class="idref" href="#should_inline:46"><span class="id" title="binder">should_inline</span></a> : <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Kernames.html#kername"><span class="id" title="definition">kername</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#bool"><span class="id" title="inductive">bool</span></a>)<br/>
(<a id="def:47" class="idref" href="#def:47"><span class="id" title="binder">def</span></a> : <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#A:45"><span class="id" title="variable">A</span></a>) : <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.TemplateMonad.Core.html#TemplateMonad"><span class="id" title="inductive">TemplateMonad</span></a> <span class="id" title="var">_</span> :=<br/>
<a id="mpath:48" class="idref" href="#mpath:48"><span class="id" title="binder">mpath</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="https://metacoq.github.io/html/MetaCoq.Template.TemplateMonad.Core.html#tmCurrentModPath"><span class="id" title="constructor">tmCurrentModPath</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#6bec7af38cdf877f357faf8f1699c8f9"><span class="id" title="notation">;;</span></a><br/>
<a id="p:49" class="idref" href="#p:49"><span class="id" title="binder">p</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="https://metacoq.github.io/html/MetaCoq.Template.TemplateMonad.Core.html#tmQuoteRecTransp"><span class="id" title="constructor">tmQuoteRecTransp</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#def:47"><span class="id" title="variable">def</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</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/>
<a id="kn:50" class="idref" href="#kn:50"><span class="id" title="binder">kn</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.Common.html#extract_def_name"><span class="id" title="definition">Common.extract_def_name</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#def:47"><span class="id" title="variable">def</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/>
<a class="idref" href="ConCert.Extraction.CertifyingInlining.html#inline_globals_template"><span class="id" title="definition">inline_globals_template</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#mpath:48"><span class="id" title="variable">mpath</span></a> (<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.declarations"><span class="id" title="projection">declarations</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#p:49"><span class="id" title="variable">p</span></a><a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.utils.MCProd.html#::pair_scope:x_'.1'"><span class="id" title="notation">.1</span></a>) <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#should_inline:46"><span class="id" title="variable">should_inline</span></a> (<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Kernames.html#KernameSet.singleton"><span class="id" title="definition">KernameSet.singleton</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#kn:50"><span class="id" title="variable">kn</span></a>).<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="template_inline" class="idref" href="#template_inline"><span class="id" title="definition">template_inline</span></a> (<a id="should_inline:51" class="idref" href="#should_inline:51"><span class="id" title="binder">should_inline</span></a> : <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Kernames.html#kername"><span class="id" title="definition">kername</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#bool"><span class="id" title="inductive">bool</span></a>): <a class="idref" href="ConCert.Extraction.Transform.html#TemplateTransform"><span class="id" title="definition">TemplateTransform</span></a> :=<br/>
<span class="id" title="keyword">fun</span> <a id="2419f67097a80bf54d8cab0e41eb773a" class="idref" href="#2419f67097a80bf54d8cab0e41eb773a"><span class="id" title="binder">Σ</span></a> => <a class="idref" href="ConCert.Extraction.ResultMonad.html#Ok"><span class="id" title="constructor">Ok</span></a> (<a class="idref" href="ConCert.Extraction.Utils.html#timed"><span class="id" title="definition">timed</span></a> "Inlining" (<span class="id" title="keyword">fun</span> <span class="id" title="var">_</span> => (<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.Build_global_env"><span class="id" title="constructor">Build_global_env</span></a> (<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.universes"><span class="id" title="projection">universes</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#2419f67097a80bf54d8cab0e41eb773a"><span class="id" title="variable">Σ</span></a>) (<a class="idref" href="ConCert.Extraction.CertifyingInlining.html#inline_globals"><span class="id" title="definition">inline_globals</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#should_inline:51"><span class="id" title="variable">should_inline</span></a> (<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Ast.html#Env.declarations"><span class="id" title="projection">declarations</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#2419f67097a80bf54d8cab0e41eb773a"><span class="id" title="variable">Σ</span></a>))))).<br/>
<br/>
<span class="id" title="keyword">Module</span> <a id="Tests" class="idref" href="#Tests"><span class="id" title="module">Tests</span></a>.<br/>
<br/>
<span class="comment">(* Inlining into the local *)</span><br/>
<span class="id" title="keyword">Module</span> <a id="Tests.Ex1" class="idref" href="#Tests.Ex1"><span class="id" title="module">Ex1</span></a>.<br/>
<span class="id" title="keyword">Definition</span> <a id="Tests.Ex1.foo" class="idref" href="#Tests.Ex1.foo"><span class="id" title="definition">foo</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#nat"><span class="id" title="inductive">nat</span></a> := <span class="id" title="keyword">fun</span> <a id="x:53" class="idref" href="#x:53"><span class="id" title="binder">x</span></a> => <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#x:53"><span class="id" title="variable">x</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> 1.<br/>
<span class="id" title="keyword">Definition</span> <a id="Tests.Ex1.bar" class="idref" href="#Tests.Ex1.bar"><span class="id" title="definition">bar</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#nat"><span class="id" title="inductive">nat</span></a> := <span class="id" title="keyword">fun</span> <a id="x:54" class="idref" href="#x:54"><span class="id" title="binder">x</span></a> => <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#Tests.Ex1.foo"><span class="id" title="definition">foo</span></a> (<a class="idref" href="ConCert.Extraction.CertifyingInlining.html#x:54"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">*</span></a> 2).<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="Tests.Ex1.baz" class="idref" href="#Tests.Ex1.baz"><span class="id" title="definition">baz</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#nat"><span class="id" title="inductive">nat</span></a> := <span class="id" title="keyword">fun</span> <a id="x:55" class="idref" href="#x:55"><span class="id" title="binder">x</span></a> => <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#Tests.Ex1.foo"><span class="id" title="definition">foo</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#x:55"><span class="id" title="variable">x</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="ConCert.Extraction.CertifyingInlining.html#Tests.Ex1.bar"><span class="id" title="definition">bar</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#x:55"><span class="id" title="variable">x</span></a>.<br/>
<br/>
<span class="id" title="var">MetaCoq</span> <span class="id" title="var">Run</span> (<a id="env:57" class="idref" href="#env:57"><span class="id" title="binder">env</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.CertifyingInlining.html#inline_def"><span class="id" title="definition">inline_def</span></a> (<span class="id" title="keyword">fun</span> <a id="kn:56" class="idref" href="#kn:56"><span class="id" title="binder">kn</span></a> => <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Kernames.html#eq_kername"><span class="id" title="abbreviation">eq_kername</span></a> <a class="idref" href="ConCert.Extraction.Common.html#f91ac6598892630a2bddbf8938e1b2db"><span class="id" title="notation"><%%</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#Tests.Ex1.foo"><span class="id" title="definition">foo</span></a> <a class="idref" href="ConCert.Extraction.Common.html#f91ac6598892630a2bddbf8938e1b2db"><span class="id" title="notation">%%></span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#kn:56"><span class="id" title="variable">kn</span></a><br/>
<a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#081ff67d3116402bb680e8692aa39185"><span class="id" title="notation">||</span></a> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Kernames.html#eq_kername"><span class="id" title="abbreviation">eq_kername</span></a> <a class="idref" href="ConCert.Extraction.Common.html#f91ac6598892630a2bddbf8938e1b2db"><span class="id" title="notation"><%%</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#Tests.Ex1.bar"><span class="id" title="definition">bar</span></a> <a class="idref" href="ConCert.Extraction.Common.html#f91ac6598892630a2bddbf8938e1b2db"><span class="id" title="notation">%%></span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#kn:56"><span class="id" title="variable">kn</span></a>)<br/>
<a class="idref" href="ConCert.Extraction.CertifyingInlining.html#Tests.Ex1.baz"><span class="id" title="definition">baz</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/>
<a id="t:58" class="idref" href="#t:58"><span class="id" title="binder">t</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="https://metacoq.github.io/html/MetaCoq.Template.TemplateMonad.Core.html#tmEval"><span class="id" title="constructor">tmEval</span></a> <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.TemplateMonad.Common.html#lazy"><span class="id" title="constructor">lazy</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="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.CertifyingInlining.html#env:57"><span class="id" title="variable">env</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/>
<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.TemplateMonad.Core.html#tmPrint"><span class="id" title="constructor">tmPrint</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#t:58"><span class="id" title="variable">t</span></a>).<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#Tests.Ex1"><span class="id" title="module">Ex1</span></a>.<br/>
<br/>
<span class="comment">(* Inlining into the definition from the standard library *)</span><br/>
<span class="id" title="keyword">Module</span> <a id="Tests.Ex2" class="idref" href="#Tests.Ex2"><span class="id" title="module">Ex2</span></a>.<br/>
<span class="id" title="var">MetaCoq</span> <span class="id" title="var">Run</span> (<a class="idref" href="ConCert.Extraction.CertifyingInlining.html#inline_def"><span class="id" title="definition">inline_def</span></a> (<span class="id" title="keyword">fun</span> <a id="kn:59" class="idref" href="#kn:59"><span class="id" title="binder">kn</span></a> => <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Kernames.html#eq_kername"><span class="id" title="abbreviation">eq_kername</span></a> <a class="idref" href="ConCert.Extraction.Common.html#f91ac6598892630a2bddbf8938e1b2db"><span class="id" title="notation"><%%</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Nat.html#add"><span class="id" title="definition">Nat.add</span></a> <a class="idref" href="ConCert.Extraction.Common.html#f91ac6598892630a2bddbf8938e1b2db"><span class="id" title="notation">%%></span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#kn:59"><span class="id" title="variable">kn</span></a> ) <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Peano.html#mult"><span class="id" title="abbreviation">mult</span></a>).<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#Tests.Ex2"><span class="id" title="module">Ex2</span></a>.<br/>
<br/>
<span class="comment">(* Inlining a function of several arguments *)</span><br/>
<span class="id" title="keyword">Module</span> <a id="Tests.Ex3" class="idref" href="#Tests.Ex3"><span class="id" title="module">Ex3</span></a>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="Tests.Ex3.foo" class="idref" href="#Tests.Ex3.foo"><span class="id" title="definition">foo</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#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#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#nat"><span class="id" title="inductive">nat</span></a> := <span class="id" title="keyword">fun</span> <a id="x:60" class="idref" href="#x:60"><span class="id" title="binder">x</span></a> <a id="y:61" class="idref" href="#y:61"><span class="id" title="binder">y</span></a> <a id="z:62" class="idref" href="#z:62"><span class="id" title="binder">z</span></a> => <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#x:60"><span class="id" title="variable">x</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="ConCert.Extraction.CertifyingInlining.html#y:61"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">*</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#z:62"><span class="id" title="variable">z</span></a>.<br/>
<span class="id" title="keyword">Definition</span> <a id="Tests.Ex3.bar" class="idref" href="#Tests.Ex3.bar"><span class="id" title="definition">bar</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#nat"><span class="id" title="inductive">nat</span></a> := <span class="id" title="keyword">fun</span> <a id="n:63" class="idref" href="#n:63"><span class="id" title="binder">n</span></a> => <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#Tests.Ex3.foo"><span class="id" title="definition">foo</span></a> (<a class="idref" href="ConCert.Extraction.CertifyingInlining.html#n:63"><span class="id" title="variable">n</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> 1) 1 <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#n:63"><span class="id" title="variable">n</span></a>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="Tests.Ex3.baz" class="idref" href="#Tests.Ex3.baz"><span class="id" title="definition">baz</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#nat"><span class="id" title="inductive">nat</span></a> := <span class="id" title="keyword">fun</span> <a id="z:64" class="idref" href="#z:64"><span class="id" title="binder">z</span></a> => <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#Tests.Ex3.bar"><span class="id" title="definition">bar</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#z:64"><span class="id" title="variable">z</span></a>.<br/>
<span class="id" title="var">MetaCoq</span> <span class="id" title="var">Run</span> (<a class="idref" href="ConCert.Extraction.CertifyingInlining.html#inline_def"><span class="id" title="definition">inline_def</span></a> (<span class="id" title="keyword">fun</span> <a id="kn:65" class="idref" href="#kn:65"><span class="id" title="binder">kn</span></a> => <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Kernames.html#eq_kername"><span class="id" title="abbreviation">eq_kername</span></a> <a class="idref" href="ConCert.Extraction.Common.html#f91ac6598892630a2bddbf8938e1b2db"><span class="id" title="notation"><%%</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#Tests.Ex3.foo"><span class="id" title="definition">foo</span></a> <a class="idref" href="ConCert.Extraction.Common.html#f91ac6598892630a2bddbf8938e1b2db"><span class="id" title="notation">%%></span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#kn:65"><span class="id" title="variable">kn</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Datatypes.html#081ff67d3116402bb680e8692aa39185"><span class="id" title="notation">||</span></a><br/>
<a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Kernames.html#eq_kername"><span class="id" title="abbreviation">eq_kername</span></a> <a class="idref" href="ConCert.Extraction.Common.html#f91ac6598892630a2bddbf8938e1b2db"><span class="id" title="notation"><%%</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#Tests.Ex3.bar"><span class="id" title="definition">bar</span></a> <a class="idref" href="ConCert.Extraction.Common.html#f91ac6598892630a2bddbf8938e1b2db"><span class="id" title="notation">%%></span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#kn:65"><span class="id" title="variable">kn</span></a>) <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#Tests.Ex3.baz"><span class="id" title="definition">baz</span></a>).<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#Tests.Ex3"><span class="id" title="module">Ex3</span></a>.<br/>
<br/>
<span class="comment">(* Records *)</span><br/>
<span class="id" title="keyword">Module</span> <a id="Tests.Ex4" class="idref" href="#Tests.Ex4"><span class="id" title="module">Ex4</span></a>.<br/>
<br/>
<span class="id" title="keyword">Set</span> <span class="id" title="var">Primitive</span> <span class="id" title="var">Projections</span>.<br/>
<span class="id" title="keyword">Record</span> <a id="Tests.Ex4.blah" class="idref" href="#Tests.Ex4.blah"><span class="id" title="record">blah</span></a> :=<br/>
{ <a id="Tests.Ex4.field1" class="idref" href="#Tests.Ex4.field1"><span class="id" title="projection">field1</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="Tests.Ex4.field2" class="idref" href="#Tests.Ex4.field2"><span class="id" title="projection">field2</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="Tests.Ex4.set_field1" class="idref" href="#Tests.Ex4.set_field1"><span class="id" title="definition">set_field1</span></a> (<a id="b:69" class="idref" href="#b:69"><span class="id" title="binder">b</span></a> : <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#Tests.Ex4.blah"><span class="id" title="record">blah</span></a>) (<a id="n:70" class="idref" href="#n:70"><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>) :=<br/>
{| <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#Tests.Ex4.field1"><span class="id" title="projection">field1</span></a> := <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#n:70"><span class="id" title="variable">n</span></a>; <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#Tests.Ex4.field2"><span class="id" title="projection">field2</span></a> := <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#b:69"><span class="id" title="variable">b</span></a>.(<a class="idref" href="ConCert.Extraction.CertifyingInlining.html#Tests.Ex4.field2"><span class="id" title="projection">field2</span></a>) |}.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="Tests.Ex4.bar" class="idref" href="#Tests.Ex4.bar"><span class="id" title="definition">bar</span></a> (<a id="b:71" class="idref" href="#b:71"><span class="id" title="binder">b</span></a> : <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#Tests.Ex4.blah"><span class="id" title="record">blah</span></a> ):= <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#Tests.Ex4.set_field1"><span class="id" title="definition">set_field1</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#b:71"><span class="id" title="variable">b</span></a> 0.<br/>
<br/>
<span class="id" title="var">MetaCoq</span> <span class="id" title="var">Run</span> (<a class="idref" href="ConCert.Extraction.CertifyingInlining.html#inline_def"><span class="id" title="definition">inline_def</span></a> (<span class="id" title="keyword">fun</span> <a id="kn:72" class="idref" href="#kn:72"><span class="id" title="binder">kn</span></a> => <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Kernames.html#eq_kername"><span class="id" title="abbreviation">eq_kername</span></a> <a class="idref" href="ConCert.Extraction.Common.html#f91ac6598892630a2bddbf8938e1b2db"><span class="id" title="notation"><%%</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#Tests.Ex4.set_field1"><span class="id" title="definition">set_field1</span></a> <a class="idref" href="ConCert.Extraction.Common.html#f91ac6598892630a2bddbf8938e1b2db"><span class="id" title="notation">%%></span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#kn:72"><span class="id" title="variable">kn</span></a>) <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#Tests.Ex4.bar"><span class="id" title="definition">bar</span></a>).<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#Tests.Ex4"><span class="id" title="module">Ex4</span></a>.<br/>
<br/>
<span class="comment">(* Casts *)</span><br/>
<span class="id" title="keyword">Module</span> <a id="Tests.Ex5" class="idref" href="#Tests.Ex5"><span class="id" title="module">Ex5</span></a>.<br/>
<span class="id" title="keyword">Definition</span> <a id="Tests.Ex5.foo" class="idref" href="#Tests.Ex5.foo"><span class="id" title="definition">foo</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#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#nat"><span class="id" title="inductive">nat</span></a> := <span class="id" title="keyword">fun</span> <a id="x:73" class="idref" href="#x:73"><span class="id" title="binder">x</span></a> <a id="y:74" class="idref" href="#y:74"><span class="id" title="binder">y</span></a> => <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#x:73"><span class="id" title="variable">x</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="ConCert.Extraction.CertifyingInlining.html#y:74"><span class="id" title="variable">y</span></a>.<br/>
<span class="id" title="keyword">Definition</span> <a id="Tests.Ex5.bar" class="idref" href="#Tests.Ex5.bar"><span class="id" title="definition">bar</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#nat"><span class="id" title="inductive">nat</span></a> := <span class="id" title="keyword">fun</span> <a id="x:75" class="idref" href="#x:75"><span class="id" title="binder">x</span></a> => ((<a class="idref" href="ConCert.Extraction.CertifyingInlining.html#Tests.Ex5.foo"><span class="id" title="definition">foo</span></a> (<a class="idref" href="ConCert.Extraction.CertifyingInlining.html#x:75"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.15.2/stdlib//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">*</span></a> 2)) : <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#nat"><span class="id" title="inductive">nat</span></a>) <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#x:75"><span class="id" title="variable">x</span></a>.<br/>
<span class="id" title="var">MetaCoq</span> <span class="id" title="var">Run</span> (<a class="idref" href="ConCert.Extraction.CertifyingInlining.html#inline_def"><span class="id" title="definition">inline_def</span></a> (<span class="id" title="keyword">fun</span> <a id="kn:76" class="idref" href="#kn:76"><span class="id" title="binder">kn</span></a> => <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Kernames.html#eq_kername"><span class="id" title="abbreviation">eq_kername</span></a> <a class="idref" href="ConCert.Extraction.Common.html#f91ac6598892630a2bddbf8938e1b2db"><span class="id" title="notation"><%%</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#Tests.Ex5.foo"><span class="id" title="definition">foo</span></a> <a class="idref" href="ConCert.Extraction.Common.html#f91ac6598892630a2bddbf8938e1b2db"><span class="id" title="notation">%%></span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#kn:76"><span class="id" title="variable">kn</span></a>) <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#Tests.Ex5.bar"><span class="id" title="definition">bar</span></a>).<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#Tests.Ex5"><span class="id" title="module">Ex5</span></a>.<br/>
<br/>
<span class="comment">(* Inlining type aliases in inductives *)</span><br/>
<span class="id" title="keyword">Module</span> <a id="Tests.Ex6" class="idref" href="#Tests.Ex6"><span class="id" title="module">Ex6</span></a>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="Tests.Ex6.my_prod" class="idref" href="#Tests.Ex6.my_prod"><span class="id" title="definition">my_prod</span></a> (<a id="A:77" class="idref" href="#A:77"><span class="id" title="binder">A</span></a> <a id="B:78" class="idref" href="#B:78"><span class="id" title="binder">B</span></a> : <span class="id" title="keyword">Type</span>) : <span class="id" title="keyword">Type</span> := <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#A:77"><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.CertifyingInlining.html#B:78"><span class="id" title="variable">B</span></a>.<br/>
<br/>
<span class="id" title="keyword">Inductive</span> <a id="Tests.Ex6.blah" class="idref" href="#Tests.Ex6.blah"><span class="id" title="inductive">blah</span></a> :=<br/>
| <a id="Tests.Ex6.blah_ctor" class="idref" href="#Tests.Ex6.blah_ctor"><span class="id" title="constructor">blah_ctor</span></a> : <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#Tests.Ex6.my_prod"><span class="id" title="definition">my_prod</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#bool"><span class="id" title="inductive">bool</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.CertifyingInlining.html#blah:79"><span class="id" title="inductive">blah</span></a>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="Tests.Ex6.foo" class="idref" href="#Tests.Ex6.foo"><span class="id" title="definition">foo</span></a> (<a id="p:81" class="idref" href="#p:81"><span class="id" title="binder">p</span></a> : <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#Tests.Ex6.my_prod"><span class="id" title="definition">my_prod</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#bool"><span class="id" title="inductive">bool</span></a>) : <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#Tests.Ex6.blah"><span class="id" title="inductive">blah</span></a> := <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#Tests.Ex6.blah_ctor"><span class="id" title="constructor">blah_ctor</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#p:81"><span class="id" title="variable">p</span></a>.<br/>
<br/>
<span class="id" title="var">MetaCoq</span> <span class="id" title="var">Run</span> (<a class="idref" href="ConCert.Extraction.CertifyingInlining.html#inline_def"><span class="id" title="definition">inline_def</span></a> (<span class="id" title="keyword">fun</span> <a id="kn:82" class="idref" href="#kn:82"><span class="id" title="binder">kn</span></a> => <a class="idref" href="https://metacoq.github.io/html/MetaCoq.Template.Kernames.html#eq_kername"><span class="id" title="abbreviation">eq_kername</span></a> <a class="idref" href="ConCert.Extraction.Common.html#f91ac6598892630a2bddbf8938e1b2db"><span class="id" title="notation"><%%</span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#Tests.Ex6.my_prod"><span class="id" title="definition">my_prod</span></a> <a class="idref" href="ConCert.Extraction.Common.html#f91ac6598892630a2bddbf8938e1b2db"><span class="id" title="notation">%%></span></a> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#kn:82"><span class="id" title="variable">kn</span></a>) <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#Tests.Ex6.foo"><span class="id" title="definition">foo</span></a>).<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#Tests.Ex6"><span class="id" title="module">Ex6</span></a>.<br/>
<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="ConCert.Extraction.CertifyingInlining.html#Tests"><span class="id" title="module">Tests</span></a>.<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>
