summaryrefslogtreecommitdiff
path: root/doc
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
Initial version
Diffstat (limited to 'doc')
-rw-r--r--doc/Makefile12
-rw-r--r--doc/Tutorial.md46
-rw-r--r--doc/pack.toml4
-rw-r--r--doc/setoid-doc.ipkg42
-rw-r--r--doc/sources/Tutorial.md11
5 files changed, 115 insertions, 0 deletions
diff --git a/doc/Makefile b/doc/Makefile
new file mode 100644
index 0000000..caaf4af
--- /dev/null
+++ b/doc/Makefile
@@ -0,0 +1,12 @@
+all: Tutorial.md
+
+.PHONY: all ttms
+
+ttms:
+ pack build setoid-doc.ipkg
+
+%.md: .PHONY
+ pack run katla markdown sources/$*.md ./build/ttc/$*.ttm > $*.md
+
+install-deps:
+ pack install-deps setoid-doc.ipkg
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>
+
diff --git a/doc/pack.toml b/doc/pack.toml
new file mode 100644
index 0000000..d555f03
--- /dev/null
+++ b/doc/pack.toml
@@ -0,0 +1,4 @@
+[doc.setoid]
+type = "local"
+path = ".."
+ipkg = "setoid.ipkg"
diff --git a/doc/setoid-doc.ipkg b/doc/setoid-doc.ipkg
new file mode 100644
index 0000000..5d183fd
--- /dev/null
+++ b/doc/setoid-doc.ipkg
@@ -0,0 +1,42 @@
+package setoid-doc
+-- version =
+authors = "Ohad Kammar"
+-- maintainers =
+-- license =
+-- brief =
+-- readme =
+-- homepage =
+-- sourceloc =
+-- bugtracker =
+
+-- the Idris2 version required (e.g. langversion >= 0.5.1)
+-- langversion
+
+-- packages to add to search path
+-- depends =
+
+modules
+ = Tutorial
+
+-- name of executable
+sourcedir = "sources"
+builddir = "build"
+outputdir = "build"
+
+-- script to run before building
+-- prebuild =
+
+-- script to run after building
+-- postbuild =
+
+-- script to run after building, before installing
+-- preinstall =
+
+-- script to run after installing
+-- postinstall =
+
+-- script to run before cleaning
+-- preclean =
+
+-- script to run after cleaning
+-- postclean =
diff --git a/doc/sources/Tutorial.md b/doc/sources/Tutorial.md
new file mode 100644
index 0000000..dc7dc71
--- /dev/null
+++ b/doc/sources/Tutorial.md
@@ -0,0 +1,11 @@
+# Tutorial: setoids
+A _setoid_ is a type equipped with an equivalence relation
+
+```idris hide
+module Tutorial
+```
+
+```idris
+Example1 : Nat
+Example1 = 0
+```