forked from lurchmath/minimal-lurch-site
-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathindex-old.html
120 lines (120 loc) · 6.94 KB
/
index-old.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
<!DOCTYPE html>
<html>
<head>
<title>Lurch Intro Tutorial</title>
<link
rel="stylesheet"
href="https://cdn.jsdelivr.net/npm/[email protected]/dist/css/bootstrap.min.css"
integrity="sha384-QWTKZyjpPEjISv5WaRU9OFeRpok6YctnYmDr5pNlyT2bRjXh0JMhjY6hW+ALEwIH"
crossorigin="anonymous"
/>
<meta name="viewport" content="width=device-width, initial-scale=1"/>
</head>
<body style="padding-top: 1em">
<div class="container">
<h1 class="alert alert-dark">Lurch Intro Tutorial</h1>
<h3 class="alert alert-primary">Who should read this?</h3>
<p>Anyone who wants a tutorial on Lurch, starting from no prior
knowledge, and covering the essential features in detail.
This tutorial is probably of greater interest to instructors
than to students, but it is open to anyone. Some of the
features covered in the tutorial also come with explanations of
the design motivations behind them.</p>
<p>Each page of this tutorial is a document you open inside the
Lurch web app itself. You can read the document and interact
with it live in the app, trying out exercises and examples posed
to you in the tutorial you're reading as you go.</p>
<p>Lurch can do much more advanced mathematics than what we showcase
in this tutorial, which starts at the beginning and tries to
move slowly and answer as many questions as possible. Other
Lurch tutorials may introduce more advanced mathematical topics
and Lurch's capability to grade them.</p>
<div class="row">
<div class="col">
<h3 class="alert alert-primary">Getting Started</h3>
<p><a href="./app/?load=../math/01-word-processor.lurch"
style="width: 100%"
class="btn btn-primary"
target="_blank">Lesson 1<br/>A word processor with math</a></p>
<p><a href="./app/?load=../math/02-meaningful-math.lurch"
style="width: 100%"
class="btn btn-primary"
target="_blank">Lesson 2<br/>Meaningful mathematics</a></p>
<p><a href="./app/"
style="width: 100%"
class="btn btn-secondary"
target="_blank">Supplement<br/>Blank document for experimentation</a></p>
</div>
<div class="col">
<h3 class="alert alert-primary">Doing math</h3>
<p><a href="./app/?load=../math/03-theorems-and-proofs.lurch"
style="width: 100%"
class="btn btn-primary"
target="_blank">Lesson 3<br/>Theorems and proofs</a></p>
<p><a href="./app/?load=../math/04-background-material.lurch"
style="width: 100%"
class="btn btn-primary"
target="_blank">Lesson 4<br/>Loading background material</a></p>
<p><a href="./app/?load=../math/propositional-logic-rules.lurch"
style="width: 100%"
class="btn btn-secondary"
target="_blank">Supplement<br/>Rules imported by Lesson 4</a></p>
<p><a href="./app/?load=../math/propositional-rules-imported.lurch"
style="width: 100%"
class="btn btn-secondary"
target="_blank">Supplement<br/>Blank document importing Lesson 4 rules</a></p>
<p><a href="./app/?load=../math/propositional-exercise-solutions.lurch"
style="width: 100%"
class="btn btn-secondary"
target="_blank">Supplement<br/>Solutions to Lesson 4 exercises</a></p>
</div>
<div class="col">
<h3 class="alert alert-primary">Higher math</h3>
<p><a href="./app/?load=../math/05-variable-declarations.lurch"
style="width: 100%"
class="btn btn-primary"
target="_blank">Lesson 5<br/>Declaring and using variables</a></p>
<p><a href="./app/?load=../math/06-real-numbers.lurch"
style="width: 100%"
class="btn btn-primary"
target="_blank">Lesson 6<br/>The real numbers</a></p>
<p><a href="./app/?load=../math/predicate-logic-rules.lurch"
style="width: 100%"
class="btn btn-secondary"
target="_blank">Supplement<br/>Rules imported by Lesson 5</a></p>
<p><a href="./app/?load=../math/predicate-rules-imported.lurch"
style="width: 100%"
class="btn btn-secondary"
target="_blank">Supplement<br/>Blank document importing Lesson 5 rules</a></p>
<p><a href="./app/?load=../math/real-numbers-rules.lurch"
style="width: 100%"
class="btn btn-secondary"
target="_blank">Supplement<br/>Rules imported by Lesson 6</a></p>
<p><a href="./app/?load=../math/real-numbers-imported.lurch"
style="width: 100%"
class="btn btn-secondary"
target="_blank">Supplement<br/>Blank document importing Lesson 6 rules</a></p>
</div>
<div class="col">
<h3 class="alert alert-primary">For instructors</h3>
<p><a href="./app/?load=../math/07-writing-rules.lurch"
style="width: 100%"
class="btn btn-primary"
target="_blank">Lesson 7<br/>Writing rules, axioms, and definitions</a></p>
<h4>Coming soon:</h4>
<p>Lessons on how to create homework assignments and other
class materials using Lurch, and publish them online as
a website for your students to use.</p>
<p>For now, some of that content is already covered
<a href="https://lurchmath.github.io/site/what-is-a-lurch-site/">on our website</a>,
and you may be interested in reading it there.</p>
</div>
</div>
</div>
<script
src="https://cdn.jsdelivr.net/npm/[email protected]/dist/js/bootstrap.bundle.min.js"
integrity="sha384-YvpcrYf0tY3lHB60NNkmXc5s9fDVZLESaAA55NDzOxhy9GkcIdslK1eN7N6jIeHz"
crossorigin="anonymous">
</script>
</body>
</html>