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