swh:1:snp:cb56ce13ac0807dbb699694ea4ec17024ae99aeb
Tip revision: e24a92af25746f6758a09ea1dc51e57491508e60 authored by Fabian Kunze on 03 February 2021, 23:29:51 UTC
added missing html doc
added missing html doc
Tip revision: e24a92a
Undecidability.L.Tactics.GenEncode.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" />
<link href="coqdoc.css" rel="stylesheet" type="text/css" />
<link href="coqdocjs.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>
<span class="button" id="toggle-proofs"></span>
<span class="right">
<a href="../">Project Page</a>
<a href="./indexpage.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="main">
<div class="code">
<span class="id" title="keyword">From</span> <span class="id" title="var">Undecidability.L</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Undecidability.L.L.html#"><span class="id" title="library">L</span></a> <a class="idref" href="Undecidability.L.Tactics.Computable.html#"><span class="id" title="library">Tactics.Computable</span></a> <a class="idref" href="Undecidability.L.Tactics.ComputableTactics.html#"><span class="id" title="library">Tactics.ComputableTactics</span></a> <a class="idref" href="Undecidability.L.Tactics.Extract.html#"><span class="id" title="library">Tactics.Extract</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">MetaCoq</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <span class="id" title="library">Template.All</span> <span class="id" title="library">TemplateMonad.Core</span> <span class="id" title="library">Template.Ast</span>.<br/>
<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Strings.String.html#"><span class="id" title="library">String</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Lists.List.html#"><span class="id" title="library">List</span></a>.<br/>
<span class="id" title="keyword">Export</span> <span class="id" title="var">String.StringSyntax</span>.<br/>
<br/>
<span class="id" title="keyword">Import</span> <span class="id" title="var">MonadNotation</span>.<br/>
<span class="id" title="keyword">Local Open</span> <span class="id" title="keyword">Scope</span> <span class="id" title="var">string_scope</span>.<br/>
<br/>
<br/>
<span class="id" title="keyword">Fixpoint</span> <a id="mkLApp" class="idref" href="#mkLApp"><span class="id" title="definition">mkLApp</span></a> (<a id="s:1" class="idref" href="#s:1"><span class="id" title="binder">s</span></a> : <span class="id" title="inductive">term</span>) (<a id="L:2" class="idref" href="#L:2"><span class="id" title="binder">L</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <span class="id" title="inductive">term</span>) :=<br/>
<span class="id" title="keyword">match</span> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#L:2"><span class="id" title="variable">L</span></a> <span class="id" title="keyword">with</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Lists.List.html#ae9a5e1034e143b218b09d8e454472bd"><span class="id" title="notation">[]</span></a> => <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#s:1"><span class="id" title="variable">s</span></a><br/>
| <span class="id" title="var">t</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#::list_scope:x_'::'_x"><span class="id" title="notation">::</span></a> <span class="id" title="var">L</span> => <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#mkLApp:3"><span class="id" title="definition">mkLApp</span></a> (<span class="id" title="constructor">tApp</span> (<span class="id" title="constructor">tConstruct</span> (<span class="id" title="constructor">mkInd</span> <a class="idref" href="Undecidability.L.Tactics.Extract.html#term_kn"><span class="id" title="definition">term_kn</span></a> 0) 1 <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Lists.List.html#ae9a5e1034e143b218b09d8e454472bd"><span class="id" title="notation">[]</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">[</span></a><a class="idref" href="Undecidability.L.Tactics.GenEncode.html#s:1"><span class="id" title="variable">s</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a> <span class="id" title="var">t</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">]</span></a>) <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#L:2"><span class="id" title="variable">L</span></a><br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="encode_arguments" class="idref" href="#encode_arguments"><span class="id" title="definition">encode_arguments</span></a> (<a id="B:5" class="idref" href="#B:5"><span class="id" title="binder">B</span></a> : <span class="id" title="inductive">term</span>) (<a id="a:6" class="idref" href="#a:6"><span class="id" title="binder">a</span></a> <a id="i:7" class="idref" href="#i:7"><span class="id" title="binder">i</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) <a id="A_j:8" class="idref" href="#A_j:8"><span class="id" title="binder">A_j</span></a> :=<br/>
<a id="A:9" class="idref" href="#A:9"><span class="id" title="binder">A</span></a> <span class="id" title="notation"><-</span> <span class="id" title="constructor">tmUnquoteTyped</span> <span class="id" title="keyword">Type</span> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#A_j:8"><span class="id" title="variable">A_j</span></a> <span class="id" title="notation">;;</span><br/>
<a id="name:10" class="idref" href="#name:10"><span class="id" title="binder">name</span></a> <span class="id" title="notation"><-</span> <span class="id" title="notation">(</span><span class="id" title="constructor">tmEval</span> <span class="id" title="constructor">cbv</span> (<a class="idref" href="Undecidability.L.Tactics.Extract.html#name_of"><span class="id" title="definition">name_of</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#A_j:8"><span class="id" title="variable">A_j</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Strings.String.html#169ad156fbc6036a53a0338819a2b301"><span class="id" title="notation">++</span></a> "_term") <span class="id" title="notation">>>=</span> <span class="id" title="constructor">Core.tmFreshName</span><span class="id" title="notation">)</span> <span class="id" title="notation">;;</span><br/>
<a id="E:11" class="idref" href="#E:11"><span class="id" title="binder">E</span></a> <span class="id" title="notation"><-</span> <a class="idref" href="Undecidability.L.Tactics.Extract.html#tmTryInfer"><span class="id" title="definition">tmTryInfer</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#name:10"><span class="id" title="variable">name</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a> (<a class="idref" href="Undecidability.L.Tactics.Extract.html#encodable"><span class="id" title="class">encodable</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#A:9"><span class="id" title="variable">A</span></a>)<span class="id" title="notation">;;</span><br/>
<a id="t:12" class="idref" href="#t:12"><span class="id" title="binder">t</span></a> <span class="id" title="notation"><-</span> <span class="id" title="method">ret</span> (@<a class="idref" href="Undecidability.L.Tactics.Extract.html#enc"><span class="id" title="method">enc</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#A:9"><span class="id" title="variable">A</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#E:11"><span class="id" title="variable">E</span></a>)<span class="id" title="notation">;;</span><br/>
<a id="l:13" class="idref" href="#l:13"><span class="id" title="binder">l</span></a> <span class="id" title="notation"><-</span> <span class="id" title="constructor">tmQuote</span> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#t:12"><span class="id" title="variable">t</span></a><span class="id" title="notation">;;</span><br/>
<span class="id" title="method">ret</span> (<span class="id" title="constructor">tApp</span> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#l:13"><span class="id" title="variable">l</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Lists.List.html#ddd65c2f7ee73ecec433744948d846bb"><span class="id" title="notation">[</span></a><span class="id" title="constructor">tRel</span> (<a class="idref" href="Undecidability.L.Tactics.GenEncode.html#a:6"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#::nat_scope:x_'-'_x"><span class="id" title="notation">-</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#i:7"><span class="id" title="variable">i</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#::nat_scope:x_'-'_x"><span class="id" title="notation">-</span></a> 1) <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Lists.List.html#ddd65c2f7ee73ecec433744948d846bb"><span class="id" title="notation">]</span></a>).<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="mkMatch" class="idref" href="#mkMatch"><span class="id" title="definition">mkMatch</span></a> (<a id="t1:14" class="idref" href="#t1:14"><span class="id" title="binder">t1</span></a> <a id="t2:15" class="idref" href="#t2:15"><span class="id" title="binder">t2</span></a> <a id="d:16" class="idref" href="#d:16"><span class="id" title="binder">d</span></a> : <span class="id" title="inductive">Ast.term</span>) (<a id="cases:17" class="idref" href="#cases:17"><span class="id" title="binder">cases</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/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.12.1/stdlib//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <span class="id" title="inductive">term</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <span class="id" title="inductive">Core.TemplateMonad</span> <span class="id" title="inductive">term</span>) :=<br/>
<a id="hs_num:18" class="idref" href="#hs_num:18"><span class="id" title="binder">hs_num</span></a> <span class="id" title="notation"><-</span> <a class="idref" href="Undecidability.L.Tactics.Extract.html#tmGetOption"><span class="id" title="definition">tmGetOption</span></a> (<a class="idref" href="Undecidability.L.Tactics.Extract.html#split_head_symbol"><span class="id" title="definition">split_head_symbol</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#t1:14"><span class="id" title="variable">t1</span></a>) "no head symbol found"<span class="id" title="notation">;;</span><br/>
<span class="id" title="keyword">let</span> '<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><span class="id" title="var">ind</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <span class="id" title="var">Params</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a> := <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#hs_num:18"><span class="id" title="variable">hs_num</span></a> <span class="id" title="tactic">in</span><br/>
<span class="id" title="keyword">let</span> <a id="params:20" class="idref" href="#params:20"><span class="id" title="binder">params</span></a> := <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Lists.List.html#length"><span class="id" title="abbreviation">List.length</span></a> <span class="id" title="var">Params</span> <span class="id" title="tactic">in</span><br/>
<a id="L:21" class="idref" href="#L:21"><span class="id" title="binder">L</span></a> <span class="id" title="notation"><-</span> <a class="idref" href="Undecidability.L.Tactics.Extract.html#list_constructors"><span class="id" title="definition">list_constructors</span></a> <span class="id" title="var">ind</span> <span class="id" title="notation">>>=</span> <span class="id" title="constructor">tmEval</span> <span class="id" title="constructor">hnf</span> <span class="id" title="notation">;;</span> <br/>
<a id="body:30" class="idref" href="#body:30"><span class="id" title="binder">body</span></a> <span class="id" title="notation"><-</span> <span class="id" title="definition">monad_map_i</span> (<span class="id" title="keyword">fun</span> <a id="i:22" class="idref" href="#i:22"><span class="id" title="binder">i</span></a> <a id="pat:26" class="idref" href="#pat:26"><span class="id" title="binder">'(</span></a><a id="pat:26" class="idref" href="#pat:26"><span class="id" title="binder">n</span></a><a id="pat:26" class="idref" href="#pat:26"><span class="id" title="binder">,</span></a> <a id="pat:26" class="idref" href="#pat:26"><span class="id" title="binder">s</span></a><a id="pat:26" class="idref" href="#pat:26"><span class="id" title="binder">,</span></a> <a id="pat:26" class="idref" href="#pat:26"><span class="id" title="binder">args</span></a><a id="pat:26" class="idref" href="#pat:26"><span class="id" title="binder">)</span></a> =><br/>
<a id="l:27" class="idref" href="#l:27"><span class="id" title="binder">l</span></a> <span class="id" title="notation"><-</span> <a class="idref" href="Undecidability.L.Tactics.Extract.html#tmArgsOfConstructor"><span class="id" title="definition">tmArgsOfConstructor</span></a> <span class="id" title="var">ind</span> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#i:22"><span class="id" title="variable">i</span></a> <span class="id" title="notation">;;</span><br/>
<a id="l':28" class="idref" href="#l':28"><span class="id" title="binder">l'</span></a> <span class="id" title="notation"><-</span> <span class="id" title="definition">monad_map_i</span> (<a class="idref" href="Undecidability.L.Tactics.Extract.html#insert_params"><span class="id" title="definition">insert_params</span></a> <a class="idref" href="Undecidability.L.Tactics.Extract.html#FUEL"><span class="id" title="abbreviation">FUEL</span></a> <span class="id" title="var">Params</span>) (<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Lists.List.html#skipn"><span class="id" title="definition">skipn</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#params:20"><span class="id" title="variable">params</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#l:27"><span class="id" title="variable">l</span></a>) <span class="id" title="notation">;;</span><br/>
<a id="t:29" class="idref" href="#t:29"><span class="id" title="binder">t</span></a> <span class="id" title="notation"><-</span> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#cases:17"><span class="id" title="variable">cases</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#i:22"><span class="id" title="variable">i</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#l':28"><span class="id" title="variable">l'</span></a> <span class="id" title="notation">;;</span> <span class="id" title="method">ret</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="Undecidability.L.Tactics.GenEncode.html#args:23"><span class="id" title="variable">args</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#t:29"><span class="id" title="variable">t</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a>) <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#L:21"><span class="id" title="variable">L</span></a> <span class="id" title="notation">;;</span> <br/>
<span class="id" title="method">ret</span> (<span class="id" title="constructor">tCase</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><span class="id" title="var">ind</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#params:20"><span class="id" title="variable">params</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a> (<span class="id" title="constructor">tLambda</span> <span class="id" title="constructor">nAnon</span> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#t1:14"><span class="id" title="variable">t1</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#t2:15"><span class="id" title="variable">t2</span></a>) <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#d:16"><span class="id" title="variable">d</span></a><br/>
<a class="idref" href="Undecidability.L.Tactics.GenEncode.html#body:30"><span class="id" title="variable">body</span></a>).<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="L_facts_mp" class="idref" href="#L_facts_mp"><span class="id" title="definition">L_facts_mp</span></a> := <span class="id" title="constructor">MPfile</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">[</span></a>"L_facts"<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a> "Util"<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a> "L"<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a> "Undecidability"<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">]</span></a>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="tmMatchCorrect" class="idref" href="#tmMatchCorrect"><span class="id" title="definition">tmMatchCorrect</span></a> (<a id="A:31" class="idref" href="#A:31"><span class="id" title="binder">A</span></a> : <span class="id" title="keyword">Type</span>) : <span class="id" title="inductive">Core.TemplateMonad</span> <span class="id" title="keyword">Prop</span> :=<br/>
<a id="t:32" class="idref" href="#t:32"><span class="id" title="binder">t</span></a> <span class="id" title="notation"><-</span> <span class="id" title="notation">(</span><span class="id" title="constructor">tmEval</span> <span class="id" title="constructor">hnf</span> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#A:31"><span class="id" title="variable">A</span></a> <span class="id" title="notation">>>=</span> <span class="id" title="constructor">tmQuote</span><span class="id" title="notation">)</span> <span class="id" title="notation">;;</span> <br/>
<a id="hs_num:33" class="idref" href="#hs_num:33"><span class="id" title="binder">hs_num</span></a> <span class="id" title="notation"><-</span> <a class="idref" href="Undecidability.L.Tactics.Extract.html#tmGetOption"><span class="id" title="definition">tmGetOption</span></a> (<a class="idref" href="Undecidability.L.Tactics.Extract.html#split_head_symbol"><span class="id" title="definition">split_head_symbol</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#t:32"><span class="id" title="variable">t</span></a>) "no inductive"<span class="id" title="notation">;;</span><br/>
<span class="id" title="keyword">let</span> '<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><span class="id" title="var">ind</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <span class="id" title="var">Params</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a> := <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#hs_num:33"><span class="id" title="variable">hs_num</span></a> <span class="id" title="tactic">in</span><br/>
<a id="num:35" class="idref" href="#num:35"><span class="id" title="binder">num</span></a> <span class="id" title="notation"><-</span> <a class="idref" href="Undecidability.L.Tactics.Extract.html#tmNumConstructors"><span class="id" title="definition">tmNumConstructors</span></a> (<span class="id" title="projection">inductive_mind</span> <span class="id" title="var">ind</span>) <span class="id" title="notation">;;</span><br/>
<a id="x:36" class="idref" href="#x:36"><span class="id" title="binder">x</span></a> <span class="id" title="notation"><-</span> <span class="id" title="constructor">Core.tmFreshName</span> "x" <span class="id" title="notation">;;</span> <br/>
<a id="mtch:42" class="idref" href="#mtch:42"><span class="id" title="binder">mtch</span></a> <span class="id" title="notation"><-</span> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#mkMatch"><span class="id" title="definition">mkMatch</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#t:32"><span class="id" title="variable">t</span></a> <a class="idref" href="Undecidability.L.Tactics.Extract.html#tTerm"><span class="id" title="definition">tTerm</span></a> (<span class="id" title="constructor">tRel</span> (2 <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">*</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#num:35"><span class="id" title="variable">num</span></a>))<br/>
(<span class="id" title="keyword">fun</span> <a id="i:37" class="idref" href="#i:37"><span class="id" title="binder">i</span></a> <a id="ctr_types:38" class="idref" href="#ctr_types:38"><span class="id" title="binder">ctr_types</span></a> => <br/>
<a id="args:39" class="idref" href="#args:39"><span class="id" title="binder">args</span></a> <span class="id" title="notation"><-</span> <span class="id" title="constructor">tmEval</span> <span class="id" title="constructor">cbv</span> (<a class="idref" href="Undecidability.Shared.Libs.PSL.Lists.BaseLists.html#2f6c87336e29315167850836a92a6885"><span class="id" title="notation">|</span></a><a class="idref" href="Undecidability.L.Tactics.GenEncode.html#ctr_types:38"><span class="id" title="variable">ctr_types</span></a><a class="idref" href="Undecidability.Shared.Libs.PSL.Lists.BaseLists.html#2f6c87336e29315167850836a92a6885"><span class="id" title="notation">|</span></a>)<span class="id" title="notation">;;</span> <br/>
<a id="C:40" class="idref" href="#C:40"><span class="id" title="binder">C</span></a> <span class="id" title="notation"><-</span> <span class="id" title="definition">monad_map_i</span> (<a class="idref" href="Undecidability.L.Tactics.GenEncode.html#encode_arguments"><span class="id" title="definition">encode_arguments</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#t:32"><span class="id" title="variable">t</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#args:39"><span class="id" title="variable">args</span></a>) <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#ctr_types:38"><span class="id" title="variable">ctr_types</span></a> <span class="id" title="notation">;;</span> <br/>
<span class="id" title="method">ret</span> (<a class="idref" href="Undecidability.L.Tactics.Extract.html#stack"><span class="id" title="definition">stack</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Lists.List.html#map"><span class="id" title="definition">map</span></a> (<span class="id" title="constructor">tLambda</span> (<span class="id" title="constructor">nAnon</span>)) <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#ctr_types:38"><span class="id" title="variable">ctr_types</span></a>)<br/>
(((<span class="id" title="keyword">fun</span> <a id="s:41" class="idref" href="#s:41"><span class="id" title="binder">s</span></a> => <a class="idref" href="Undecidability.L.Tactics.Extract.html#mkAppList"><span class="id" title="definition">mkAppList</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#s:41"><span class="id" title="variable">s</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#C:40"><span class="id" title="variable">C</span></a>) (<span class="id" title="constructor">tRel</span> (<a class="idref" href="Undecidability.L.Tactics.GenEncode.html#args:39"><span class="id" title="variable">args</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> 2 <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">*</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">(</span></a><a class="idref" href="Undecidability.L.Tactics.GenEncode.html#num:35"><span class="id" title="variable">num</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#::nat_scope:x_'-'_x"><span class="id" title="notation">-</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#i:37"><span class="id" title="variable">i</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#::nat_scope:x_'-'_x"><span class="id" title="notation">-</span></a> 1)))))<br/>
) <span class="id" title="notation">;;</span><br/>
<a id="E':43" class="idref" href="#E':43"><span class="id" title="binder">E'</span></a> <span class="id" title="notation"><-</span> <span class="id" title="constructor">Core.tmInferInstance</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a> (<a class="idref" href="Undecidability.L.Tactics.Extract.html#encodable"><span class="id" title="class">encodable</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#A:31"><span class="id" title="variable">A</span></a>)<span class="id" title="notation">;;</span><br/>
<a id="E:44" class="idref" href="#E:44"><span class="id" title="binder">E</span></a> <span class="id" title="notation"><-</span> <a class="idref" href="Undecidability.L.Tactics.Extract.html#tmGetMyOption"><span class="id" title="definition">tmGetMyOption</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#E':43"><span class="id" title="variable">E'</span></a> "failed" <span class="id" title="notation">;;</span> <br/>
<a id="t':45" class="idref" href="#t':45"><span class="id" title="binder">t'</span></a> <span class="id" title="notation"><-</span> <span class="id" title="method">ret</span> (@<a class="idref" href="Undecidability.L.Tactics.Extract.html#enc"><span class="id" title="method">enc</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#A:31"><span class="id" title="variable">A</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#E:44"><span class="id" title="variable">E</span></a>)<span class="id" title="notation">;;</span><br/>
<a id="l:46" class="idref" href="#l:46"><span class="id" title="binder">l</span></a> <span class="id" title="notation"><-</span> <span class="id" title="constructor">tmQuote</span> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#t':45"><span class="id" title="variable">t'</span></a><span class="id" title="notation">;;</span><br/>
<a id="encn:47" class="idref" href="#encn:47"><span class="id" title="binder">encn</span></a> <span class="id" title="notation"><-</span> <span class="id" title="method">ret</span> (<span class="id" title="constructor">tApp</span> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#l:46"><span class="id" title="variable">l</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Lists.List.html#ddd65c2f7ee73ecec433744948d846bb"><span class="id" title="notation">[</span></a><span class="id" title="constructor">tRel</span> (2<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">*</span></a><a class="idref" href="Undecidability.L.Tactics.GenEncode.html#num:35"><span class="id" title="variable">num</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Lists.List.html#ddd65c2f7ee73ecec433744948d846bb"><span class="id" title="notation">]</span></a>) <span class="id" title="notation">;;</span><br/>
<a id="lhs:51" class="idref" href="#lhs:51"><span class="id" title="binder">lhs</span></a> <span class="id" title="notation"><-</span> <span class="id" title="method">ret</span> (<a class="idref" href="Undecidability.L.Tactics.GenEncode.html#mkLApp"><span class="id" title="definition">mkLApp</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#encn:47"><span class="id" title="variable">encn</span></a> ((<span class="id" title="keyword">fix</span> <span class="id" title="var">f</span> <a id="n:48" class="idref" href="#n:48"><span class="id" title="binder">n</span></a> := <span class="id" title="keyword">match</span> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#n:48"><span class="id" title="variable">n</span></a> <span class="id" title="keyword">with</span> 0 => <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Lists.List.html#ae9a5e1034e143b218b09d8e454472bd"><span class="id" title="notation">[]</span></a> | <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <span class="id" title="var">n</span> => <span class="id" title="constructor">tRel</span> (2 <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">*</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#n:48"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> 1) <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#::list_scope:x_'::'_x"><span class="id" title="notation">::</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#f:49"><span class="id" title="variable">f</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#n:48"><span class="id" title="variable">n</span></a> <span class="id" title="keyword">end</span> ) <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#num:35"><span class="id" title="variable">num</span></a>)) <span class="id" title="notation">;;</span><br/>
<a id="ter:53" class="idref" href="#ter:53"><span class="id" title="binder">ter</span></a> <span class="id" title="notation"><-</span> <span class="id" title="method">ret</span> (<span class="id" title="constructor">tProd</span> <span class="id" title="constructor">nAnon</span> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#t:32"><span class="id" title="variable">t</span></a> (<a class="idref" href="Undecidability.Shared.Libs.PSL.Numbers.html#it"><span class="id" title="definition">it</span></a> (<span class="id" title="keyword">fun</span> <a id="s:52" class="idref" href="#s:52"><span class="id" title="binder">s</span></a> : <span class="id" title="inductive">term</span> => <span class="id" title="constructor">tProd</span> <span class="id" title="constructor">nAnon</span> <a class="idref" href="Undecidability.L.Tactics.Extract.html#tTerm"><span class="id" title="definition">tTerm</span></a> (<span class="id" title="constructor">tProd</span> <span class="id" title="constructor">nAnon</span> (<span class="id" title="constructor">tApp</span> (<span class="id" title="constructor">tConst</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="Undecidability.L.Tactics.GenEncode.html#L_facts_mp"><span class="id" title="definition">L_facts_mp</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> "proc"<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Lists.List.html#ae9a5e1034e143b218b09d8e454472bd"><span class="id" title="notation">[]</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Lists.List.html#ddd65c2f7ee73ecec433744948d846bb"><span class="id" title="notation">[</span></a><span class="id" title="constructor">tRel</span> 0<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Lists.List.html#ddd65c2f7ee73ecec433744948d846bb"><span class="id" title="notation">]</span></a>) <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#s:52"><span class="id" title="variable">s</span></a>)) <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#num:35"><span class="id" title="variable">num</span></a> ((<span class="id" title="constructor">tApp</span> (<span class="id" title="constructor">tConst</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="Undecidability.L.Tactics.GenEncode.html#L_facts_mp"><span class="id" title="definition">L_facts_mp</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> "redLe"<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Lists.List.html#ae9a5e1034e143b218b09d8e454472bd"><span class="id" title="notation">[]</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">[</span></a><a class="idref" href="Undecidability.L.Tactics.Extract.html#mkNat"><span class="id" title="definition">mkNat</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#num:35"><span class="id" title="variable">num</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#lhs:51"><span class="id" title="variable">lhs</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#mtch:42"><span class="id" title="variable">mtch</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">]</span></a>))))<span class="id" title="notation">;;</span><br/>
<a id="ter:54" class="idref" href="#ter:54"><span class="id" title="binder">ter</span></a> <span class="id" title="notation"><-</span> <span class="id" title="constructor">tmEval</span> <span class="id" title="constructor">cbv</span> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#ter:53"><span class="id" title="variable">ter</span></a> <span class="id" title="notation">;;</span><br/>
<span class="id" title="constructor">tmUnquoteTyped</span> <span class="id" title="keyword">Prop</span> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#ter:54"><span class="id" title="variable">ter</span></a>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="matchlem" class="idref" href="#matchlem"><span class="id" title="definition">matchlem</span></a> <a id="n:55" class="idref" href="#n:55"><span class="id" title="binder">n</span></a> <a id="A:56" class="idref" href="#A:56"><span class="id" title="binder">A</span></a> := (<span class="id" title="constructor">Core.tmBind</span> (<a class="idref" href="Undecidability.L.Tactics.GenEncode.html#tmMatchCorrect"><span class="id" title="definition">tmMatchCorrect</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#A:56"><span class="id" title="variable">A</span></a>) (<span class="id" title="keyword">fun</span> <a id="m:57" class="idref" href="#m:57"><span class="id" title="binder">m</span></a> => <span class="id" title="constructor">tmLemma</span> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#n:55"><span class="id" title="variable">n</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#m:57"><span class="id" title="variable">m</span></a> <span class="id" title="notation">;;</span> <span class="id" title="method">ret</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#tt"><span class="id" title="constructor">tt</span></a>)).<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="tmGenEncode" class="idref" href="#tmGenEncode"><span class="id" title="definition">tmGenEncode</span></a> (<a id="n:58" class="idref" href="#n:58"><span class="id" title="binder">n</span></a> : <span class="id" title="definition">ident</span>) (<a id="A:59" class="idref" href="#A:59"><span class="id" title="binder">A</span></a> : <span class="id" title="keyword">Type</span>) : <span class="id" title="inductive">TemplateMonad</span> (<a class="idref" href="Undecidability.L.Tactics.Extract.html#encodable"><span class="id" title="class">encodable</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#A:59"><span class="id" title="variable">A</span></a>) :=<br/>
<a id="e:60" class="idref" href="#e:60"><span class="id" title="binder">e</span></a> <span class="id" title="notation"><-</span> <a class="idref" href="Undecidability.L.Tactics.Extract.html#tmEncode"><span class="id" title="definition">tmEncode</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#A:59"><span class="id" title="variable">A</span></a><span class="id" title="notation">;;</span><br/>
<a id="modpath:61" class="idref" href="#modpath:61"><span class="id" title="binder">modpath</span></a> <span class="id" title="notation"><-</span> <span class="id" title="constructor">tmCurrentModPath</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#tt"><span class="id" title="constructor">tt</span></a> <span class="id" title="notation">;;</span><br/>
<a id="p:63" class="idref" href="#p:63"><span class="id" title="binder">p</span></a> <span class="id" title="notation"><-</span> <span class="id" title="constructor">Core.tmLemma</span> (<a class="idref" href="Undecidability.L.Tactics.GenEncode.html#n:58"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Strings.String.html#169ad156fbc6036a53a0338819a2b301"><span class="id" title="notation">++</span></a> "_proc") (<span class="id" title="keyword">forall</span> <a id="x:62" class="idref" href="#x:62"><span class="id" title="binder">x</span></a> : <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#A:59"><span class="id" title="variable">A</span></a>, <a class="idref" href="Undecidability.L.Util.L_facts.html#proc"><span class="id" title="definition">proc</span></a> (<a class="idref" href="Undecidability.L.Tactics.GenEncode.html#e:60"><span class="id" title="variable">e</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#x:62"><span class="id" title="variable">x</span></a>)) <span class="id" title="notation">;;</span><br/>
<a id="n3:64" class="idref" href="#n3:64"><span class="id" title="binder">n3</span></a> <span class="id" title="notation"><-</span> <span class="id" title="constructor">tmEval</span> <span class="id" title="constructor">cbv</span> ("encodable_" <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Strings.String.html#169ad156fbc6036a53a0338819a2b301"><span class="id" title="notation">++</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#n:58"><span class="id" title="variable">n</span></a>) <span class="id" title="notation">;;</span><br/>
<a id="d:65" class="idref" href="#d:65"><span class="id" title="binder">d</span></a> <span class="id" title="notation"><-</span> <a class="idref" href="Undecidability.L.Tactics.Extract.html#tmInstanceRed"><span class="id" title="definition">tmInstanceRed</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#n3:64"><span class="id" title="variable">n3</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a> (<a class="idref" href="Undecidability.L.Tactics.Extract.html#mk_encodable"><span class="id" title="constructor">mk_encodable</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#p:63"><span class="id" title="variable">p</span></a>)<span class="id" title="notation">;;</span><br/>
<a id="m:66" class="idref" href="#m:66"><span class="id" title="binder">m</span></a> <span class="id" title="notation"><-</span> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#tmMatchCorrect"><span class="id" title="definition">tmMatchCorrect</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#A:59"><span class="id" title="variable">A</span></a><span class="id" title="notation">;;</span><br/>
<a id="n4:67" class="idref" href="#n4:67"><span class="id" title="binder">n4</span></a> <span class="id" title="notation"><-</span> <span class="id" title="constructor">tmEval</span> <span class="id" title="constructor">cbv</span> (<a class="idref" href="Undecidability.L.Tactics.GenEncode.html#n:58"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Strings.String.html#169ad156fbc6036a53a0338819a2b301"><span class="id" title="notation">++</span></a> "_correct") <span class="id" title="notation">;;</span><br/>
<span class="id" title="constructor">Core.tmBind</span> (<a class="idref" href="Undecidability.L.Tactics.GenEncode.html#tmMatchCorrect"><span class="id" title="definition">tmMatchCorrect</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#A:59"><span class="id" title="variable">A</span></a>) (<span class="id" title="keyword">fun</span> <a id="m':68" class="idref" href="#m':68"><span class="id" title="binder">m'</span></a> => <span class="id" title="constructor">tmLemma</span> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#n4:67"><span class="id" title="variable">n4</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#m':68"><span class="id" title="variable">m'</span></a><span class="id" title="notation">;;</span><span class="id" title="method">ret</span> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#d:65"><span class="id" title="variable">d</span></a>).<br/>
<br/>
<span class="id" title="var">Arguments</span> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#tmGenEncode"><span class="id" title="definition">tmGenEncode</span></a> <span class="id" title="var">_</span>%<span class="id" title="var">string</span> <span class="id" title="var">_</span>%<span class="id" title="keyword">type</span>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="tmGenEncodeInj" class="idref" href="#tmGenEncodeInj"><span class="id" title="definition">tmGenEncodeInj</span></a> (<a id="n:69" class="idref" href="#n:69"><span class="id" title="binder">n</span></a> : <span class="id" title="definition">ident</span>) (<a id="A:70" class="idref" href="#A:70"><span class="id" title="binder">A</span></a> : <span class="id" title="keyword">Type</span>) : <span class="id" title="inductive">TemplateMonad</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a> :=<br/>
<a id="d:71" class="idref" href="#d:71"><span class="id" title="binder">d</span></a> <span class="id" title="notation"><-</span> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#tmGenEncode"><span class="id" title="definition">tmGenEncode</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#n:69"><span class="id" title="variable">n</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#A:70"><span class="id" title="variable">A</span></a><span class="id" title="notation">;;</span><br/>
<a id="n2:72" class="idref" href="#n2:72"><span class="id" title="binder">n2</span></a> <span class="id" title="notation"><-</span> <span class="id" title="constructor">tmEval</span> <span class="id" title="constructor">cbv</span> ((<a class="idref" href="Undecidability.L.Tactics.GenEncode.html#n:69"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Strings.String.html#169ad156fbc6036a53a0338819a2b301"><span class="id" title="notation">++</span></a> "_inj"))<span class="id" title="notation">;;</span><br/>
<a id="i:73" class="idref" href="#i:73"><span class="id" title="binder">i</span></a> <span class="id" title="notation"><-</span> <span class="id" title="constructor">Core.tmLemma</span> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#n2:72"><span class="id" title="variable">n2</span></a> (@<a class="idref" href="Undecidability.L.Tactics.Computable.html#encInj"><span class="id" title="class">encInj</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#A:70"><span class="id" title="variable">A</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#d:71"><span class="id" title="variable">d</span></a>)<span class="id" title="notation">;;</span><br/>
<a id="n3:74" class="idref" href="#n3:74"><span class="id" title="binder">n3</span></a> <span class="id" title="notation"><-</span> <span class="id" title="constructor">tmEval</span> <span class="id" title="constructor">cbv</span> ("encInj_" <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Strings.String.html#169ad156fbc6036a53a0338819a2b301"><span class="id" title="notation">++</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#n:69"><span class="id" title="variable">n</span></a>) <span class="id" title="notation">;;</span><br/>
<a id="d:75" class="idref" href="#d:75"><span class="id" title="binder">d</span></a> <span class="id" title="notation"><-</span> <a class="idref" href="Undecidability.L.Tactics.Extract.html#tmInstanceRed"><span class="id" title="definition">tmInstanceRed</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#n3:74"><span class="id" title="variable">n3</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#i:73"><span class="id" title="variable">i</span></a><span class="id" title="notation">;;</span><br/>
<span class="id" title="method">ret</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#tt"><span class="id" title="constructor">tt</span></a>.<br/>
<br/>
<span class="id" title="var">Arguments</span> <a class="idref" href="Undecidability.L.Tactics.GenEncode.html#tmGenEncodeInj"><span class="id" title="definition">tmGenEncodeInj</span></a> <span class="id" title="var">_</span>%<span class="id" title="var">string</span> <span class="id" title="var">_</span>%<span class="id" title="keyword">type</span>.<br/>
<br/>
<br/>
<span class="id" title="keyword">Global</span> <span class="id" title="keyword">Obligation</span> <span class="id" title="keyword">Tactic</span> := <span class="id" title="keyword">match</span> <span class="id" title="keyword">goal</span> <span class="id" title="keyword">with</span><br/>
| [ |- <span class="id" title="keyword">forall</span> <a id="x:77" class="idref" href="#x:77"><span class="id" title="binder">x</span></a> : ?<span class="id" title="var">X</span>, <a class="idref" href="Undecidability.L.Util.L_facts.html#proc"><span class="id" title="definition">proc</span></a> ?<span class="id" title="var">f</span> ] => <span class="id" title="tactic">try</span> <span class="id" title="var">register_proc</span><br/>
| [ |- <a class="idref" href="Undecidability.L.Tactics.Computable.html#encInj"><span class="id" title="class">encInj</span></a> <span class="id" title="var">_</span> ] => <span class="id" title="tactic">unfold</span> <a class="idref" href="Undecidability.L.Tactics.Computable.html#encInj"><span class="id" title="class">encInj</span></a>;<span class="id" title="var">register_inj</span><br/>
| [ |- <a class="idref" href="Undecidability.Shared.Libs.PSL.Bijection.html#injective"><span class="id" title="definition">injective</span></a> ?<span class="id" title="var">f</span> ] => <span class="id" title="var">register_inj</span><br/>
| [ |- <span class="id" title="keyword">context</span> [<span class="id" title="var">_</span> <a class="idref" href="Undecidability.L.Util.L_facts.html#3be01d9c5dfac7c25a9d8a86545f2019"><span class="id" title="notation">>(<=</span></a> <span class="id" title="var">_</span><a class="idref" href="Undecidability.L.Util.L_facts.html#3be01d9c5dfac7c25a9d8a86545f2019"><span class="id" title="notation">)</span></a> <span class="id" title="var">_</span>] ] => <span class="id" title="var">extract</span> <span class="id" title="keyword">match</span><br/>
<span class="id" title="keyword">end</span> || <span class="id" title="var">Tactics.program_simpl</span>.<br/>
<br/>
</div>
</div>
<div id="footer">
Generated by <a href="http://coq.inria.fr/">coqdoc</a> and improved with <a href="https://github.com/tebbi/coqdocjs">CoqdocJS</a>
</div>
</div>
</body>
</html>
