diff --git a/README.md b/README.md index d1c20225..8b452fef 100644 --- a/README.md +++ b/README.md @@ -4,26 +4,22 @@ title: About permalink: /about/ --- -This is a rewrite of the text +This is a rewrite of the text [Software Foundations]( +https://softwarefoundations.cis.upenn.edu/current/index.html +) +from Coq to Agda. The authors are +[Wen Kokke]( +https://github.com/wenkokke +) +and +[Philip Wadler]( +http://homepages.inf.ed.ac.uk/wadler/ +). -* [Software Foundations]( - https://softwarefoundations.cis.upenn.edu/current/index.html - ) -from Coq to Agda. The authors are +## How to host literate code -* [Wen Kokke]( - https://github.com/wenkokke - ) -* [Philip Wadler]( - http://homepages.inf.ed.ac.uk/wadler/ - ) - -## Instructions - -_How to host literate code_ - -In directory `sf/` the following: +In directory `sf/` run the following: $ make clobber $ make @@ -33,19 +29,20 @@ The visible page appears at localhost:4000/sf/ +## Markdown + For markdown commands see [Daring Fireball]( https://daringfireball.net/projects/markdown/syntax ). -_Important git commands_ +## Important git commands git pull git commit -am "message" git push -_[Unicode abbreviations]( -https://github.com/agda/agda/blob/master/src/data/emacs-mode/agda-input.el#L194 -)_ +## Unicode abbreviations + \to → \u+ ⊎ @@ -54,13 +51,20 @@ https://github.com/agda/agda/blob/master/src/data/emacs-mode/agda-input.el#L194 x\_1 x₁ x\_i xᵢ -_Bindings for [Agda mode]( -http://agda.readthedocs.io/en/latest/tools/emacs-mode.html -)_ +Also see [here]( +https://github.com/agda/agda/blob/master/src/data/emacs-mode/agda-input.el#L194 +). + +## Bindings for Agda mode ? create hole {!...!} create holde C-c C-l reload C-c C-c x split on variable x C-c C-space fill in hole - + + +Also see [here]( +http://agda.readthedocs.io/en/latest/tools/emacs-mode.html +). + diff --git a/index.md b/index.md index 0aa92552..750defcf 100644 --- a/index.md +++ b/index.md @@ -2,21 +2,18 @@ title : Table of Contents layout : page --- - -This is a rewrite of the text -* [Software Foundations]( - https://softwarefoundations.cis.upenn.edu/current/index.html - ) - -from Coq to Agda. The authors are - -* [Wen Kokke]( - https://github.com/wenkokke - ) -* [Philip Wadler]( - http://homepages.inf.ed.ac.uk/wadler/ - ) +This is a rewrite of the text [Software Foundations]( +https://softwarefoundations.cis.upenn.edu/current/index.html +) +from Coq to Agda. The authors are +[Wen Kokke]( +https://github.com/wenkokke +) +and +[Philip Wadler]( +http://homepages.inf.ed.ac.uk/wadler/ +). ## Contents