summaryrefslogtreecommitdiff
path: root/doc/Tutorial.md
diff options
context:
space:
mode:
authorOhad Kammar <ohad.kammar@ed.ac.uk>2022-08-07 18:23:04 +0100
committerOhad Kammar <ohad.kammar@ed.ac.uk>2022-08-07 18:23:04 +0100
commitefd5f75c0672773341b5ca1c1d4b2ad0c0d09daa (patch)
treee22ef47d908efd30f985d47e6abfa53d6c6189b5 /doc/Tutorial.md
Initial version
Diffstat (limited to 'doc/Tutorial.md')
-rw-r--r--doc/Tutorial.md46
1 files changed, 46 insertions, 0 deletions
diff --git a/doc/Tutorial.md b/doc/Tutorial.md
new file mode 100644
index 0000000..20678f2
--- /dev/null
+++ b/doc/Tutorial.md
@@ -0,0 +1,46 @@
+<style>
+.IdrisData {
+ color: darkred
+}
+.IdrisType {
+ color: blue
+}
+.IdrisBound {
+ color: black
+}
+.IdrisFunction {
+ color: darkgreen
+}
+.IdrisKeyword {
+ text-decoration: underline;
+}
+.IdrisComment {
+ color: #b22222
+}
+.IdrisNamespace {
+ font-style: italic;
+ color: black
+}
+.IdrisPostulate {
+ font-weight: bold;
+ color: red
+}
+.IdrisModule {
+ font-style: italic;
+ color: black
+}
+.IdrisCode {
+ display: block;
+ background-color: whitesmoke;
+}
+</style>
+# Tutorial: setoids
+A _setoid_ is a type equipped with an equivalence relation
+
+
+
+<code class="IdrisCode">
+<span class="IdrisFunction">F</span>&nbsp;<span class="IdrisKeyword">:</span>&nbsp;<span class="IdrisType">Nat</span><br />
+<span class="IdrisFunction">F</span>&nbsp;<span class="IdrisKeyword">=</span>&nbsp;<span class="IdrisData">0</span><br />
+</code>
+