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

added unicode names

Browse source
This commit is contained in:
wadler 2017-07-24 12:05:21 +01:00
parent a96c961727
commit 844d39fef0
2 changed files with 3203 additions and 3195 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6470
out/Stlc.md
View file

File diff suppressed because it is too large Load diff

6
src/Stlc.lagda
View file

@ -183,7 +183,7 @@ irrelevant. Thus the five terms
* `` λ[ f ∶ 𝔹 ⇒ 𝔹 ] λ[ x ∶ 𝔹 ] ` f · (` f · ` x) `` * `` λ[ f ∶ 𝔹 ⇒ 𝔹 ] λ[ x ∶ 𝔹 ] ` f · (` f · ` x) ``
* `` λ[ g ∶ 𝔹 ⇒ 𝔹 ] λ[ y ∶ 𝔹 ] ` g · (` g · ` y) `` * `` λ[ g ∶ 𝔹 ⇒ 𝔹 ] λ[ y ∶ 𝔹 ] ` g · (` g · ` y) ``
* `` λ[ fred ∶ 𝔹 ⇒ 𝔹 ] λ[ xander ∶ 𝔹 ] ` fred · (` fred · ` xander) `` * `` λ[ fred ∶ 𝔹 ⇒ 𝔹 ] λ[ xander ∶ 𝔹 ] ` fred · (` fred · ` xander) ``
* `` λ[ 👿 ∶ 𝔹 ⇒ 𝔹 ] λ[ 😄 ∶ 𝔹 ] ` 👿 · (` 👿 · ` 😄) `` * `` λ[ 😈 ∶ 𝔹 ⇒ 𝔹 ] λ[ 😄 ∶ 𝔹 ] ` 😈 · (` 😈 · ` 😄) ``
* `` λ[ x ∶ 𝔹 ⇒ 𝔹 ] λ[ f ∶ 𝔹 ] ` x · (` x · ` f) `` * `` λ[ x ∶ 𝔹 ⇒ 𝔹 ] λ[ f ∶ 𝔹 ] ` x · (` x · ` f) ``
are all considered equivalent. This equivalence relation are all considered equivalent. This equivalence relation
@ -222,6 +222,10 @@ variables in a term are distinct from the free variables, which can
avoid confusions that may arise if bound and free variables have the avoid confusions that may arise if bound and free variables have the
same names. same names.
#### Special characters
😈 U+1F608: SMILING FACE WITH HORNS
😄 U+1F604: SMILING FACE WITH OPEN MOUTH AND SMILING EYES
#### Precedence #### Precedence