michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

finished learning for Tuesday

Browse source
This commit is contained in:
wadler 2017-03-21 16:42:39 +00:00
parent c11978a133
commit a594a73198
4 changed files with 49 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

43
README.md
View file

@ -4,4 +4,45 @@ title: About
permalink: /about/ permalink: /about/
--- ---
We should put something here. How to host literal code.
In directory `sf/` run both the following in background:
$ jekyll serve &
$ watch make &
The visible page appears at
localhost:4000/sf/<permalink>
For markdown commands see [Daring Fireball](
https://daringfireball.net/projects/markdown/syntax
).
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
).
\to →
\u+ ⊎
\all ∀
\x ×
x\_1 x₁
x\_i xᵢ
Bindings for [Agda mode](
http://agda.readthedocs.io/en/latest/tools/emacs-mode.html
)
? 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

8
out/Maps.md
View file

@ -119,7 +119,7 @@ standard library, wherever they overlap.
>;</a >;</a
><a name="1631" ><a name="1631"
> </a > </a
><a name="1632" href="https://agda.github.io/agda-stdlib/Data.Empty.html#360" class="Function" ><a name="1632" href="https://agda.github.io/agda-stdlib/Data.Empty.html#348" class="Function"
>&#8869;-elim</a >&#8869;-elim</a
><a name="1638" class="Symbol" ><a name="1638" class="Symbol"
>)</a >)</a
@ -1615,7 +1615,7 @@ back $$v$$:
>=</a >=</a
><a name="6306" ><a name="6306"
> </a > </a
><a name="6307" href="https://agda.github.io/agda-stdlib/Data.Empty.html#360" class="Function" ><a name="6307" href="https://agda.github.io/agda-stdlib/Data.Empty.html#348" class="Function"
>&#8869;-elim</a >&#8869;-elim</a
><a name="6313" ><a name="6313"
> </a > </a
@ -1818,7 +1818,7 @@ the same result that $$m$$ would have given:
>=</a >=</a
><a name="6726" ><a name="6726"
> </a > </a
><a name="6727" href="https://agda.github.io/agda-stdlib/Data.Empty.html#360" class="Function" ><a name="6727" href="https://agda.github.io/agda-stdlib/Data.Empty.html#348" class="Function"
>&#8869;-elim</a >&#8869;-elim</a
><a name="6733" ><a name="6733"
> </a > </a
@ -3067,7 +3067,7 @@ updates.
>=</a >=</a
><a name="8919" ><a name="8919"
> </a > </a
><a name="8920" href="https://agda.github.io/agda-stdlib/Data.Empty.html#360" class="Function" ><a name="8920" href="https://agda.github.io/agda-stdlib/Data.Empty.html#348" class="Function"
>&#8869;-elim</a >&#8869;-elim</a
><a name="8926" ><a name="8926"
> </a > </a

2
out/Stlc.md
View file

@ -83,7 +83,7 @@ permalink : /Stlc
>;</a >;</a
><a name="234" ><a name="234"
> </a > </a
><a name="235" href="https://agda.github.io/agda-stdlib/Data.Empty.html#360" class="Function" ><a name="235" href="https://agda.github.io/agda-stdlib/Data.Empty.html#348" class="Function"
>&#8869;-elim</a >&#8869;-elim</a
><a name="241" class="Symbol" ><a name="241" class="Symbol"
>)</a >)</a

4
out/StlcProp.md
View file

@ -55,7 +55,7 @@ permalink : /StlcProp
>;</a >;</a
><a name="193" ><a name="193"
> </a > </a
><a name="194" href="https://agda.github.io/agda-stdlib/Data.Empty.html#360" class="Function" ><a name="194" href="https://agda.github.io/agda-stdlib/Data.Empty.html#348" class="Function"
>&#8869;-elim</a >&#8869;-elim</a
><a name="200" class="Symbol" ><a name="200" class="Symbol"
>)</a >)</a
@ -2708,7 +2708,7 @@ _Proof_: We show, by induction on the proof that $$x$$ appears
>=</a >=</a
><a name="10391" ><a name="10391"
> </a > </a
><a name="10392" href="https://agda.github.io/agda-stdlib/Data.Empty.html#360" class="Function" ><a name="10392" href="https://agda.github.io/agda-stdlib/Data.Empty.html#348" class="Function"
>&#8869;-elim</a >&#8869;-elim</a
><a name="10398" ><a name="10398"
> </a > </a