1
1
<!DOCTYPE html>
2
2
< html >
3
- < head >
3
+ < head >
4
4
< title > Coq Platform Docs - Demo</ title >
5
- </ head >
6
- < body >
5
+ < meta charset ="utf8 "/>
6
+ < link rel ="stylesheet " href ="style.css "/>
7
+ < link rel ="shortcut icon " href ="images/coq-community-logo.ico " type ="image/x-icon ">
8
+ </ head >
9
+ < body >
7
10
< h1 > Coq Platform Docs - Demo</ h1 >
11
+
12
+ < div style ="text-align:left ">
13
+ < img src ="images/github-mark.png " height ="25 " style ="border:0px ">
14
+ < a href ="https://github.com/Zimmi48/platform-docs ">
15
+ View Coq-Platform-Doc
16
+ </ a >
17
+ < img src ="images/github-mark.png " height ="25 " style ="border:0px ">
18
+ </ div >
19
+
20
+ < h2 id ="about "> About</ h2 >
21
+ < p > < a href ="https://coq.inria.fr "> < img src ="images/coq-community-logo.png " align ="right " width ="100 "> </ a > </ p >
8
22
< p >
9
- This is a demo page for the Coq Platform Docs.
23
+ This is a demo page for the Coq Platform Docs.
24
+ These tutorials are meant to become part of Rocq's next website and the
25
+ github repository should be part of the Coq organization.
10
26
</ p >
11
27
< p >
12
- List of available tutorials:
28
+ The interactive versions can be run in a web browser, for the source code,
29
+ one needs a text editor able to interact with Coq (e.g. CoqIDE, emacs with
30
+ Proof General, vim with CoqTail, vscode with vscoq).
13
31
</ p >
32
+
33
+ < h2 id ="coq-tut "> Coq Tutorials</ h2 >
14
34
< ul >
15
- < li > < a href ="RequireImportTutorial.html "> Require/Import Tutorial (interactive version)</ a > </ li >
16
- < li > < a href ="RequireImportTutorial.v "> Require/Import Tutorial (source code)</ a > </ li >
17
- < li > < a href ="SearchTutorial.html "> Search Tutorial (interactive version)</ a > </ li >
18
- < li > < a href ="SearchTutorial.v "> Search Tutorial (source code)</ a > </ li >
19
- < li > < a href ="Tutorial_Equations_basics.html "> Equations Tutorial : basics (interactive version)</ a > </ li >
20
- < li > < a href ="Tutorial_Equations_basics.v "> Equations Tutorial : basics (source code)</ a > </ li >
21
- < li > < a href ="Tutorial_Equations_Obligations.html "> Equations Tutorial : obligations (interactive version)</ a > </ li >
22
- < li > < a href ="Tutorial_Equations_Obligations.v "> Equations Tutorial : obligations (source code)</ a > </ li >
23
- < li > < a href ="Tutorial_Equations_wf.html "> Equations Tutorial : well-founded recursion (interactive version)</ a > </ li >
24
- < li > < a href ="Tutorial_Equations_wf.v "> Equations Tutorial : well-founded recursion (source code)</ a > </ li >
35
+ < li >
36
+ Search Tutorial:
37
+ < a href ="SearchTutorial.html "> interactive version</ a >
38
+ and
39
+ < a href ="SearchTutorial.v "> source code</ a >
40
+ </ li >
41
+ < li >
42
+ Basic library files and module management:
43
+ < a href ="RequireImportTutorial.html "> interactive version</ a >
44
+ and
45
+ < a href ="RequireImportTutorial.v "> source code</ a >
46
+ </ li >
25
47
</ ul >
26
- </ body >
27
- </ html >
48
+
49
+ < h2 id =eq-tut > Equations tutorials</ h2 >
50
+ < ul >
51
+ < li >
52
+ Basics:
53
+ < a href ="Tutorial_Equations_basics.html "> interactive version</ a >
54
+ and
55
+ < a href ="Tutorial_Equations_basics.v "> source code</ a >
56
+ </ li >
57
+ < li >
58
+ Obligations:
59
+ < a href ="Tutorial_Equations_Obligations.html "> interactive version</ a >
60
+ and
61
+ < a href ="Tutorial_Equations_Obligations.v "> source code</ a >
62
+ </ li >
63
+ < li >
64
+ Well-founded recursion:
65
+ < a href ="Tutorial_Equations_wf.html "> interactive version</ a >
66
+ and
67
+ < a href ="Tutorial_Equations_wf.v "> source code</ a >
68
+ </ li >
69
+ </ ul >
70
+ </ body >
71
+ </ html >
0 commit comments