Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
913770c
commit 101ae21
Showing
4 changed files
with
47 additions
and
33 deletions.
There are no files selected for viewing
This file was deleted.
Oops, something went wrong.
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 |
---|---|---|
@@ -0,0 +1,41 @@ | ||
FAQ | ||
=== | ||
|
||
|
||
Why adopt a style guide? | ||
------------------------ | ||
|
||
TODO | ||
|
||
|
||
When is the right time to adopt a style guide? | ||
---------------------------------------------- | ||
|
||
TODO | ||
|
||
|
||
Why adopt *this* style guide? | ||
----------------------------- | ||
|
||
TODO | ||
|
||
|
||
What is Alectryon? | ||
------------------ | ||
|
||
`Alectryon <https://github.com/cpitclaudel/alectryon/>`_ is a tool for processing Coq files and generating pretty output for use in HTML, PDF, and other formats. | ||
|
||
When used to generate HTML, it allows readers to step-through the intermediate goal states of proofs using :command:`ctrl+↓` and :command:`ctrl+↑` or by hovering the mouse cursor over a particular line. Try it now: | ||
|
||
.. coq:: | ||
|
||
Lemma le_l : forall y x, S x <= y -> x <= y. | ||
induction y; inversion 1; subst. | ||
all: info_eauto. | ||
Qed. | ||
|
||
|
||
How can I contribute to this guide? | ||
----------------------------------- | ||
|
||
`vstyle is hosted on GitHub <https://github.com/appliedfm/vstyle>`_. Information about how to contribute can be found in `our CONTRIBUTING.md file <https://github.com/appliedfm/vstyle/blob/main/CONTRIBUTING.md>`_. |
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
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -13,7 +13,7 @@ About | |
:maxdepth: 3 | ||
|
||
principles | ||
alectryon_examples | ||
faq | ||
|
||
|
||
Code Style | ||
|