-
Notifications
You must be signed in to change notification settings - Fork 1
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Documentation of branch “master” at 55a3746c
- Loading branch information
Showing
278 changed files
with
1,303 additions
and
1,303 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,6 +1,6 @@ | ||
| <!DOCTYPE html> | ||
| <html xmlns="http://www.w3.org/1999/xhtml"><head><title>Cooking (rocq-runtime.Cooking)</title><link rel="stylesheet" href="../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.0.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../index.html">rocq-runtime</a> » Cooking</nav><header class="odoc-preamble"><h1>Module <code><span>Cooking</span></code></h1></header><nav class="odoc-toc"><ul><li><a href="#data-needed-to-abstract-over-the-section-variables-and-section-universes">Data needed to abstract over the section variables and section universes</a></li></ul></nav><div class="odoc-content"><h6 id="data-needed-to-abstract-over-the-section-variables-and-section-universes"><a href="#data-needed-to-abstract-over-the-section-variables-and-section-universes" class="anchor"></a>Data needed to abstract over the section variables and section universes</h6><p>The instantiation to apply to generalized declarations so that they behave as if not generalized: this is the a1..an instance to apply to a declaration c in the following transformation: <code>a1:T1..an:Tn, C:U(a1..an) ⊢ v(a1..an,C):V(a1..an,C) | ||
| ~~> | ||
| C:Πx1..xn.U(x1..xn), a1:T1..an:Tn ⊢ v(a1..an,Ca1..an):V(a1..an,Ca1..an)</code> note that the data looks close to the one for substitution above (because the substitution are represented by their domain) but here, local definitions of the context have been dropped</p><div class="odoc-spec"><div class="spec type" id="type-abstr_inst_info" class="anchored"><a href="#type-abstr_inst_info" class="anchor"></a><code><span><span class="keyword">type</span> abstr_inst_info</span></code></div></div><div class="odoc-spec"><div class="spec type" id="type-entry_map" class="anchored"><a href="#type-entry_map" class="anchor"></a><code><span><span class="keyword">type</span> <span>'a entry_map</span></span><span> = <span><span class="type-var">'a</span> <a href="../Names/Cmap/index.html#type-t">Names.Cmap.t</a></span> * <span><span class="type-var">'a</span> <a href="../Names/Mindmap/index.html#type-t">Names.Mindmap.t</a></span></span></code></div></div><div class="odoc-spec"><div class="spec type" id="type-expand_info" class="anchored"><a href="#type-expand_info" class="anchor"></a><code><span><span class="keyword">type</span> expand_info</span><span> = <span><a href="#type-abstr_inst_info">abstr_inst_info</a> <a href="#type-entry_map">entry_map</a></span></span></code></div></div><p>The collection of instantiations to be done on generalized declarations + the generalization to be done on a specific judgment: <code>a1:T1,a2:T2,C:U(a1) ⊢ v(a1,a2,C):V(a1,a2,C) | ||
| C:Πx1..xn.U(x1..xn), a1:T1..an:Tn ⊢ v(a1..an,Ca1..an):V(a1..an,Ca1..an)</code> note that the data looks close to the one for substitution above (because the substitution are represented by their domain) but here, local definitions of the context have been dropped</p><div class="odoc-spec"><div class="spec type" id="type-abstr_inst_info" class="anchored"><a href="#type-abstr_inst_info" class="anchor"></a><code><span><span class="keyword">type</span> abstr_inst_info</span></code></div></div><div class="odoc-spec"><div class="spec type" id="type-entry_map" class="anchored"><a href="#type-entry_map" class="anchor"></a><code><span><span class="keyword">type</span> <span>'a entry_map</span></span><span> = <span><span class="type-var">'a</span> <a href="../Names/Cmap_env/index.html#type-t">Names.Cmap_env.t</a></span> * <span><span class="type-var">'a</span> <a href="../Names/Mindmap_env/index.html#type-t">Names.Mindmap_env.t</a></span></span></code></div></div><div class="odoc-spec"><div class="spec type" id="type-expand_info" class="anchored"><a href="#type-expand_info" class="anchor"></a><code><span><span class="keyword">type</span> expand_info</span><span> = <span><a href="#type-abstr_inst_info">abstr_inst_info</a> <a href="#type-entry_map">entry_map</a></span></span></code></div></div><p>The collection of instantiations to be done on generalized declarations + the generalization to be done on a specific judgment: <code>a1:T1,a2:T2,C:U(a1) ⊢ v(a1,a2,C):V(a1,a2,C) | ||
| ~~> | ||
| c:Πx.U(x) ⊢ λx1x2.(v(a1,a2,cx1)[a1,a2:=x1,x2]):Πx1x2.(V(a1,a2,ca1)[a1,a2:=x1,x2])</code> so, a cooking_info is the map <code>c ↦ x1..xn</code>, the context x:T,y:U to generalize, and the substitution <code>x,y</code></p><div class="odoc-spec"><div class="spec type" id="type-cooking_info" class="anchored"><a href="#type-cooking_info" class="anchor"></a><code><span><span class="keyword">type</span> cooking_info</span></code></div></div><div class="odoc-spec"><div class="spec value" id="val-empty_cooking_info" class="anchored"><a href="#val-empty_cooking_info" class="anchor"></a><code><span><span class="keyword">val</span> empty_cooking_info : <a href="#type-cooking_info">cooking_info</a></span></code></div><div class="spec-doc"><p>Nothing to abstract</p></div></div><div class="odoc-spec"><div class="spec value" id="val-make_cooking_info" class="anchored"><a href="#val-make_cooking_info" class="anchor"></a><code><span><span class="keyword">val</span> make_cooking_info : <span>recursive:<span><a href="../Names/MutInd/index.html#type-t">Names.MutInd.t</a> option</span> <span class="arrow">-></span></span> <span><a href="#type-expand_info">expand_info</a> <span class="arrow">-></span></span> <span><a href="../Constr/index.html#type-named_context">Constr.named_context</a> <span class="arrow">-></span></span> <span><a href="../UVars/UContext/index.html#type-t">UVars.UContext.t</a> <span class="arrow">-></span></span> <a href="#type-cooking_info">cooking_info</a> * <a href="#type-abstr_inst_info">abstr_inst_info</a></span></code></div><div class="spec-doc"><p>Abstract a context assumed to be de-Bruijn free for terms and universes</p></div></div><div class="odoc-spec"><div class="spec value" id="val-names_info" class="anchored"><a href="#val-names_info" class="anchor"></a><code><span><span class="keyword">val</span> names_info : <span><a href="#type-cooking_info">cooking_info</a> <span class="arrow">-></span></span> <a href="../Names/Id/Set/index.html#type-t">Names.Id.Set.t</a></span></code></div></div><div class="odoc-spec"><div class="spec value" id="val-universe_context_of_cooking_info" class="anchored"><a href="#val-universe_context_of_cooking_info" class="anchor"></a><code><span><span class="keyword">val</span> universe_context_of_cooking_info : <span><a href="#type-cooking_info">cooking_info</a> <span class="arrow">-></span></span> <a href="../UVars/AbstractContext/index.html#type-t">UVars.AbstractContext.t</a></span></code></div></div><div class="odoc-spec"><div class="spec value" id="val-instance_of_cooking_info" class="anchored"><a href="#val-instance_of_cooking_info" class="anchor"></a><code><span><span class="keyword">val</span> instance_of_cooking_info : <span><a href="#type-cooking_info">cooking_info</a> <span class="arrow">-></span></span> <span><a href="../Constr/index.html#type-t">Constr.t</a> array</span></span></code></div></div><div class="odoc-spec"><div class="spec type" id="type-cooking_cache" class="anchored"><a href="#type-cooking_cache" class="anchor"></a><code><span><span class="keyword">type</span> cooking_cache</span></code></div></div><div class="odoc-spec"><div class="spec value" id="val-create_cache" class="anchored"><a href="#val-create_cache" class="anchor"></a><code><span><span class="keyword">val</span> create_cache : <span><a href="#type-cooking_info">cooking_info</a> <span class="arrow">-></span></span> <a href="#type-cooking_cache">cooking_cache</a></span></code></div></div><div class="odoc-spec"><div class="spec value" id="val-instance_of_cooking_cache" class="anchored"><a href="#val-instance_of_cooking_cache" class="anchor"></a><code><span><span class="keyword">val</span> instance_of_cooking_cache : <span><a href="#type-cooking_cache">cooking_cache</a> <span class="arrow">-></span></span> <span><a href="../Constr/index.html#type-t">Constr.t</a> array</span></span></code></div></div><div class="odoc-spec"><div class="spec value" id="val-rel_context_of_cooking_cache" class="anchored"><a href="#val-rel_context_of_cooking_cache" class="anchor"></a><code><span><span class="keyword">val</span> rel_context_of_cooking_cache : <span><a href="#type-cooking_cache">cooking_cache</a> <span class="arrow">-></span></span> <a href="../Constr/index.html#type-rel_context">Constr.rel_context</a></span></code></div></div><div class="odoc-spec"><div class="spec value" id="val-abstract_as_type" class="anchored"><a href="#val-abstract_as_type" class="anchor"></a><code><span><span class="keyword">val</span> abstract_as_type : <span><a href="#type-cooking_cache">cooking_cache</a> <span class="arrow">-></span></span> <span><a href="../Constr/index.html#type-types">Constr.types</a> <span class="arrow">-></span></span> <a href="../Constr/index.html#type-types">Constr.types</a></span></code></div></div><div class="odoc-spec"><div class="spec value" id="val-abstract_as_body" class="anchored"><a href="#val-abstract_as_body" class="anchor"></a><code><span><span class="keyword">val</span> abstract_as_body : <span><a href="#type-cooking_cache">cooking_cache</a> <span class="arrow">-></span></span> <span><a href="../Constr/index.html#type-constr">Constr.constr</a> <span class="arrow">-></span></span> <a href="../Constr/index.html#type-constr">Constr.constr</a></span></code></div></div><div class="odoc-spec"><div class="spec value" id="val-abstract_as_sort" class="anchored"><a href="#val-abstract_as_sort" class="anchor"></a><code><span><span class="keyword">val</span> abstract_as_sort : <span><a href="#type-cooking_cache">cooking_cache</a> <span class="arrow">-></span></span> <span><a href="../Sorts/index.html#type-t">Sorts.t</a> <span class="arrow">-></span></span> <a href="../Sorts/index.html#type-t">Sorts.t</a></span></code></div></div><div class="odoc-spec"><div class="spec value" id="val-lift_mono_univs" class="anchored"><a href="#val-lift_mono_univs" class="anchor"></a><code><span><span class="keyword">val</span> lift_mono_univs : <span><a href="#type-cooking_info">cooking_info</a> <span class="arrow">-></span></span> <span><a href="../Univ/ContextSet/index.html#type-t">Univ.ContextSet.t</a> <span class="arrow">-></span></span> <a href="#type-cooking_info">cooking_info</a> * <a href="../Univ/ContextSet/index.html#type-t">Univ.ContextSet.t</a></span></code></div></div><div class="odoc-spec"><div class="spec value" id="val-lift_poly_univs" class="anchored"><a href="#val-lift_poly_univs" class="anchor"></a><code><span><span class="keyword">val</span> lift_poly_univs : <span><a href="#type-cooking_info">cooking_info</a> <span class="arrow">-></span></span> <span><a href="../UVars/AbstractContext/index.html#type-t">UVars.AbstractContext.t</a> <span class="arrow">-></span></span> <a href="#type-cooking_info">cooking_info</a> * <span>(int * int)</span> * <a href="../UVars/AbstractContext/index.html#type-t">UVars.AbstractContext.t</a></span></code></div><div class="spec-doc"><p>The <code>int</code> is how many universes got discharged, ie size of returned context - size of input context.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-lift_private_mono_univs" class="anchored"><a href="#val-lift_private_mono_univs" class="anchor"></a><code><span><span class="keyword">val</span> lift_private_mono_univs : <span><a href="#type-cooking_info">cooking_info</a> <span class="arrow">-></span></span> <span><span class="type-var">'a</span> <span class="arrow">-></span></span> <span class="type-var">'a</span></span></code></div></div><div class="odoc-spec"><div class="spec value" id="val-lift_private_poly_univs" class="anchored"><a href="#val-lift_private_poly_univs" class="anchor"></a><code><span><span class="keyword">val</span> lift_private_poly_univs : <span><a href="#type-cooking_info">cooking_info</a> <span class="arrow">-></span></span> <span><a href="../Univ/ContextSet/index.html#type-t">Univ.ContextSet.t</a> <span class="arrow">-></span></span> <a href="../Univ/ContextSet/index.html#type-t">Univ.ContextSet.t</a></span></code></div></div><div class="odoc-spec"><div class="spec value" id="val-discharge_proj_repr" class="anchored"><a href="#val-discharge_proj_repr" class="anchor"></a><code><span><span class="keyword">val</span> discharge_proj_repr : <span><a href="#type-cooking_info">cooking_info</a> <span class="arrow">-></span></span> <span><a href="../Names/Projection/Repr/index.html#type-t">Names.Projection.Repr.t</a> <span class="arrow">-></span></span> <a href="../Names/Projection/Repr/index.html#type-t">Names.Projection.Repr.t</a></span></code></div></div></div></body></html> |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.