diff options
| author | ymherklotz <ymherklotz@users.noreply.github.com> | 2021-01-22 17:23:49 +0000 |
|---|---|---|
| committer | ymherklotz <ymherklotz@users.noreply.github.com> | 2021-01-22 17:23:49 +0000 |
| commit | aca7b8f57370ccdba41577c845361800ae6f8d39 (patch) | |
| tree | 266b4381bf09663c6ce53e7d3201565fb4f77e19 /coq-style-guide | |
| parent | ab7b1393ef5fc0c5c74485bae78344572a71e4be (diff) | |
| download | vericert-docs-aca7b8f57370ccdba41577c845361800ae6f8d39.tar.gz vericert-docs-aca7b8f57370ccdba41577c845361800ae6f8d39.zip | |
deploy: 1ff8b1c7a3f3e37809e9ac8c1e21d50df270696a
Diffstat (limited to 'coq-style-guide')
| -rw-r--r-- | coq-style-guide/index.html | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/coq-style-guide/index.html b/coq-style-guide/index.html index 5fa7532..7272741 100644 --- a/coq-style-guide/index.html +++ b/coq-style-guide/index.html @@ -1,6 +1,6 @@ <!doctype html><html lang=en><head><meta name=generator content="Hugo 0.80.0"><meta charset=utf-8><meta name=viewport content="width=device-width,initial-scale=1"><meta name=description content="This style guide was taken from Silveroak, it outlines code style for Coq code in this repository. There are certainly other valid strategies and opinions on Coq code style; this is laid out purely in the name of consistency. For a visual example of the style, see the example at the bottom of this file. Code organization # Legal banner # Files should begin with a copyright/license banner, as shown in the example above."><meta name=theme-color content="#FFFFFF"><meta property="og:title" content="Coq Style Guide"><meta property="og:description" content="This style guide was taken from Silveroak, it outlines code style for Coq code in this repository. There are certainly other valid strategies and opinions on Coq code style; this is laid out purely in the name of consistency. For a visual example of the style, see the example at the bottom of this file. -Code organization # Legal banner # Files should begin with a copyright/license banner, as shown in the example above."><meta property="og:type" content="article"><meta property="og:url" content="https://vericert.ymhg.org/coq-style-guide/"><title>Coq Style Guide | Vericert</title><link rel=manifest href=/manifest.json><link rel=icon href=/favicon.png type=image/x-icon><link rel=stylesheet href=/book.min.cc7f7da4e201466c24d4145b227311a8f1462dd7940d82e2d55c370645cf9541.css integrity="sha256-zH99pOIBRmwk1BRbInMRqPFGLdeUDYLi1Vw3BkXPlUE="><script defer src=/en.search.min.0954d4b2fc6bff27e6f999bbc5c4fd9011adb3be3811a6642db8ce343b98ef63.js integrity="sha256-CVTUsvxr/yfm+Zm7xcT9kBGts744EaZkLbjONDuY72M="></script></head><body><input type=checkbox class="hidden toggle" id=menu-control> +Code organization # Legal banner # Files should begin with a copyright/license banner, as shown in the example above."><meta property="og:type" content="article"><meta property="og:url" content="https://vericert.ymhg.org/coq-style-guide/"><title>Coq Style Guide | Vericert</title><link rel=manifest href=/manifest.json><link rel=icon href=/favicon.png type=image/x-icon><link rel=stylesheet href=/book.min.cc7f7da4e201466c24d4145b227311a8f1462dd7940d82e2d55c370645cf9541.css integrity="sha256-zH99pOIBRmwk1BRbInMRqPFGLdeUDYLi1Vw3BkXPlUE="><script defer src=/en.search.min.d59155e62a5c5b4ff8f90845580f2225b938da2b1506af250727aadcdc5122f1.js integrity="sha256-1ZFV5ipcW0/4+QhFWA8iJbk42isVBq8lByeq3NxRIvE="></script></head><body><input type=checkbox class="hidden toggle" id=menu-control> <input type=checkbox class="hidden toggle" id=toc-control><main class="container flex"><aside class=book-menu><nav><h2 class=book-brand><a href=/><span>Vericert</span></a></h2><div class=book-search><input type=text id=book-search-input placeholder=Search aria-label=Search maxlength=64 data-hotkeys=s/><div class="book-search-spinner hidden"></div><ul id=book-search-results></ul></div><ul><li><a href=https://vericert.ymhg.org/coq-style-guide/ class=active>Coq Style Guide</a></li><li><a href=https://vericert.ymhg.org/docs/>Docs</a><ul><li><a href=https://vericert.ymhg.org/docs/building/>Building Vericert</a></li><li><a href=https://vericert.ymhg.org/docs/using-vericert/>Using Vericert</a></li></ul></li></ul><ul><li><a href=https://github.com/ymherklotz/vericert target=_blank rel=noopener>Github</a></li></ul></nav><script>(function(){var menu=document.querySelector("aside.book-menu nav");addEventListener("beforeunload",function(event){localStorage.setItem("menu.scrollTop",menu.scrollTop);});menu.scrollTop=localStorage.getItem("menu.scrollTop");})();</script></aside><div class=book-page><header class=book-header><div class="flex align-center justify-between"><label for=menu-control><img src=/svg/menu.svg class=book-icon alt=Menu></label> <strong>Coq Style Guide</strong> <label for=toc-control><img src=/svg/toc.svg class=book-icon alt="Table of Contents"></label></div><aside class="hidden clearfix"><nav id=TableOfContents><ul><li><ul><li><a href=#code-organization>Code organization</a><ul><li><a href=#legal-banner>Legal banner</a></li><li><a href=#import-statements>Import statements</a></li><li><a href=#notations-and-scopes>Notations and scopes</a></li></ul></li><li><a href=#formatting>Formatting</a><ul><li><a href=#line-length>Line length</a></li><li><a href=#whitespace-and-indentation>Whitespace and indentation</a></li></ul></li><li><a href=#definitions-and-fixpoints>Definitions and Fixpoints</a></li><li><a href=#inductives>Inductives</a></li><li><a href=#lemmatheorem-statements>Lemma/Theorem statements</a></li><li><a href=#proofs-and-tactics>Proofs and tactics</a></li><li><a href=#naming>Naming</a></li><li><a href=#example>Example</a></li></ul></li></ul></nav></aside></header><article class=markdown><p>This style guide was taken from <a href=https://github.com/project-oak/silveroak>Silveroak</a>, it outlines code style for Coq code @@ -59,7 +59,8 @@ arguments, align the next line with the first argument:</p><div class=highlight> <span class=o>|</span> <span class=o>|-</span> <span class=n>context</span> <span class=o>[</span><span class=n>eq</span><span class=o>]</span> <span class=o>=></span> <span class=kr>idtac</span> <span class=k>end</span><span class=o>.</span> </code></pre></div></li></ul><h2 id=definitions-and-fixpoints>Definitions and Fixpoints -<a class=anchor href=#definitions-and-fixpoints>#</a></h2><ul><li>It’s okay to leave the return type of <code>Definition=s and =Fixpoint=s implicit (e.g. =Definition x :</code> 5= instead of <code>Definition x : nat :</code> 5=) when the type is +<a class=anchor href=#definitions-and-fixpoints>#</a></h2><ul><li>It’s okay to leave the return type of <code>Definition</code>’s and <code>Fixpoint</code>’s implicit +(e.g. <code>Definition x := 5</code> instead of <code>Definition x : nat := 5</code>) when the type is very simple or obvious (for instance, the definition is in a file which deals exclusively with operations on <code>Z</code>).</li></ul><h2 id=inductives>Inductives <a class=anchor href=#inductives>#</a></h2><ul><li><p>The <code>.</code> ending an <code>Inductive</code> can be either on the same line as the last case or @@ -93,7 +94,7 @@ of reasoning in large proofs.</li></ul></li><li><p>If invoking a tactic that is tactic no longer solves as many subgoals as expected (or unexpectedly solves more).</li></ul></li><li><p>If invoking a string of tactics (composed by <code>;</code>) that will break the goal into multiple subgoals and then solve all but one, still use <code>[ ]</code> to enforce that -all but one goal is solved.</p><ul><li>Example: <code>split; try lia; [ ]</code>.</li></ul></li><li><p>Tactics that consist only of <code>repeat=ing a procedure (e.g. =repeat match</code>, +all but one goal is solved.</p><ul><li>Example: <code>split; try lia; [ ]</code>.</li></ul></li><li><p>Tactics that consist only of <code>repeat</code>-ing a procedure (e.g. <code>repeat match</code>, <code>repeat first</code>) should factor out a single step of that procedure a separate tactic called <code><tactic name>_step</code>, because the single-step version is much easier to debug. For instance:</p><div class=highlight><pre class=chroma><code class=language-coq data-lang=coq><span class=kn>Ltac</span> <span class=n>crush_step</span> <span class=o>:=</span> |