diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/Makefile | 12 | ||||
| -rw-r--r-- | doc/Tutorial.md | 46 | ||||
| -rw-r--r-- | doc/pack.toml | 4 | ||||
| -rw-r--r-- | doc/setoid-doc.ipkg | 42 | ||||
| -rw-r--r-- | doc/sources/Tutorial.md | 11 |
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> <span class="IdrisKeyword">:</span> <span class="IdrisType">Nat</span><br /> +<span class="IdrisFunction">F</span> <span class="IdrisKeyword">=</span> <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 +``` |