Skip to main content

Browse the archive

https://github.com/uds-psl/cook-levin
20 March 2024, 19:14:53 UTC
Raw File
Tip revision: e24a92af25746f6758a09ea1dc51e57491508e60 authored by Fabian Kunze on 03 February 2021, 23:29:51 UTC
added missing html doc
Tip revision: e24a92a
Undecidability.L.Complexity.LinDecode.LTD_def.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.Tactics</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Undecidability.L.Tactics.LTactics.html#"><span class="id" title="library">LTactics</span></a>.<br/>

<br/>
<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.Functions.Decoding.html#"><span class="id" title="library">Functions.Decoding</span></a>.<br/>

<br/>
<span class="id" title="keyword">Class</span> <a id="linTimeDecodable" class="idref" href="#linTimeDecodable"><span class="id" title="record">linTimeDecodable</span></a> `(<a id="X:1" class="idref" href="#X:1"><span class="id" title="binder">X</span></a>:<span class="id" title="keyword">Type</span>) `{<a id="H0:3" class="idref" href="#H0:3"><span class="id" title="binder">decodable</span></a> <a id="H0:3" class="idref" href="#H0:3"><span class="id" title="binder">X</span></a>}: <span class="id" title="keyword">Type</span> :=<br/>
&nbsp;&nbsp;{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a id="c__linDec" class="idref" href="#c__linDec"><span class="id" title="projection">c__linDec</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>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a id="comp_enc_lin" class="idref" href="#comp_enc_lin"><span class="id" title="projection">comp_enc_lin</span></a> : <a class="idref" href="Undecidability.L.Tactics.ComputableTime.html#:::'computableTime'''_x"><span class="id" title="notation">computableTime'</span></a> <a class="idref" href="Undecidability.L.Tactics.ComputableTime.html#:::'computableTime'''_x"><span class="id" title="notation">(</span></a><a class="idref" href="Undecidability.L.Functions.Decoding.html#decode"><span class="id" title="method">decode</span></a> <a class="idref" href="Undecidability.L.Complexity.LinDecode.LTD_def.html#X:1"><span class="id" title="variable">X</span></a><a class="idref" href="Undecidability.L.Tactics.ComputableTime.html#:::'computableTime'''_x"><span class="id" title="notation">)</span></a> <a class="idref" href="Undecidability.L.Tactics.ComputableTime.html#:::'computableTime'''_x"><span class="id" title="notation">(</span></a><a class="idref" href="Undecidability.L.Tactics.ComputableTime.html#:::'computableTime'''_x"><span class="id" title="notation">fun</span></a> <a id="x:6" class="idref" href="#x:6"><span class="id" title="binder">x</span></a> <a class="idref" href="Undecidability.L.Tactics.ComputableTime.html#:::'computableTime'''_x"><span class="id" title="notation">_</span></a> <a class="idref" href="Undecidability.L.Tactics.ComputableTime.html#:::'computableTime'''_x"><span class="id" title="notation">=&gt;</span></a> <a class="idref" href="Undecidability.L.Tactics.ComputableTime.html#:::'computableTime'''_x"><span class="id" title="notation">(</span></a><a class="idref" href="Undecidability.L.Tactics.ComputableTime.html#:::'computableTime'''_x"><span class="id" title="notation">size</span></a> <a class="idref" href="Undecidability.L.Tactics.ComputableTime.html#:::'computableTime'''_x"><span class="id" title="notation">x</span></a> <a class="idref" href="Undecidability.L.Tactics.ComputableTime.html#:::'computableTime'''_x"><span class="id" title="notation">*</span></a><a class="idref" href="Undecidability.L.Tactics.ComputableTime.html#:::'computableTime'''_x"><span class="id" title="notation">c__linDec</span></a> <a class="idref" href="Undecidability.L.Tactics.ComputableTime.html#:::'computableTime'''_x"><span class="id" title="notation">+</span></a> <a class="idref" href="Undecidability.L.Tactics.ComputableTime.html#:::'computableTime'''_x"><span class="id" title="notation">c__linDec</span></a><a class="idref" href="Undecidability.L.Tactics.ComputableTime.html#:::'computableTime'''_x"><span class="id" title="notation">,</span></a><a class="idref" href="Undecidability.L.Tactics.ComputableTime.html#:::'computableTime'''_x"><span class="id" title="notation">tt</span></a><a class="idref" href="Undecidability.L.Tactics.ComputableTime.html#:::'computableTime'''_x"><span class="id" title="notation">))</span></a>;<br/>
&nbsp;&nbsp;}.<br/>

<br/>
<span class="id" title="var">Arguments</span> <a class="idref" href="Undecidability.L.Complexity.LinDecode.LTD_def.html#linTimeDecodable"><span class="id" title="class">linTimeDecodable</span></a> : <span class="id" title="tactic">clear</span> <span class="id" title="var">implicits</span>.<br/>
<span class="id" title="var">Arguments</span> <a class="idref" href="Undecidability.L.Complexity.LinDecode.LTD_def.html#linTimeDecodable"><span class="id" title="class">linTimeDecodable</span></a> <span class="id" title="var">_</span> {<span class="id" title="var">_</span> <span class="id" title="var">_</span>}.<br/>

<br/>
<span class="id" title="var">Arguments</span> <a class="idref" href="Undecidability.L.Complexity.LinDecode.LTD_def.html#c__linDec"><span class="id" title="method">c__linDec</span></a> : <span class="id" title="tactic">clear</span> <span class="id" title="var">implicits</span>.<br/>
<span class="id" title="var">Arguments</span> <a class="idref" href="Undecidability.L.Complexity.LinDecode.LTD_def.html#c__linDec"><span class="id" title="method">c__linDec</span></a> <span class="id" title="var">_</span> {<span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span>}.<br/>

<br/>
<span class="id" title="var">Existing</span> <span class="id" title="keyword">Instance</span> <span class="id" title="var">comp_enc_lin</span>.<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>
back to top