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

Publishing draft of Logic

Browse source
This commit is contained in:
wadler 2018-01-26 14:37:46 -02:00
parent 6beb810138
commit 4e0aeabfe4
16 changed files with 51053 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
index.md
View file

@ -15,7 +15,7 @@ and
http://homepages.inf.ed.ac.uk/wadler/
).
## Contents
## Part 1: Logical Foundations
<!--
- [Basics: Functional Programming in Agda]({{ "/Basics" | relative_url }})
@ -23,9 +23,14 @@ http://homepages.inf.ed.ac.uk/wadler/
- [Naturals: Natural numbers]({{ "/Naturals" | relative_url }})
- [Properties: Proof by induction]({{ "/Properties" | relative_url }})
- [PropertiesEx: Solutions to exercises]({{ "/PropertiesEx" | relative_url }})
- [PropertiesAns: Solutions to exercises]({{ "/PropertiesAns" | relative_url }})
- [Relations: Inductive Definition of Relations]({{ "/Relations" | relative_url }})
- [RelationsEx: Solutions to exercises]({{ "/RelationsEx" | relative_url }})
- [RelationsAns: Solutions to exercises]({{ "/RelationsAns" | relative_url }})
- [Logic: Logic]({{ "/Logic" | relative_url }})
- [LogicAns: Solutions to exercises]({{ "/LogicAns" | relative_url }})
## Part 2: Programming Language Foundations
- [Maps: Total and Partial Maps]({{ "/Maps" | relative_url }})
- [Stlc: The Simply Typed Lambda-Calculus]({{ "/Stlc" | relative_url }})
- [StlcProp: Properties of STLC]({{ "/StlcProp" | relative_url }})

1617
out/Basics0.md Normal file
View file

File diff suppressed because it is too large Load diff

2205
out/Exercises.md Normal file
View file

File diff suppressed because it is too large Load diff

13058
out/Logic.md Normal file
View file

File diff suppressed because it is too large Load diff

1024
out/LogicAns.md Normal file
View file

File diff suppressed because it is too large Load diff

6329
out/Maps.md Normal file
View file

File diff suppressed because it is too large Load diff

1153
out/Naturals.md Normal file
View file

File diff suppressed because it is too large Load diff

1280
out/Properties.md Normal file
View file

File diff suppressed because it is too large Load diff

1517
out/PropertiesAns.md Normal file
View file

File diff suppressed because it is too large Load diff

1517
out/PropertiesEx.md Normal file
View file

File diff suppressed because it is too large Load diff

3615
out/Relations.md Normal file
View file

File diff suppressed because it is too large Load diff

2133
out/RelationsAns.md Normal file
View file

File diff suppressed because it is too large Load diff

2133
out/RelationsEx.md Normal file
View file

File diff suppressed because it is too large Load diff

5684
out/Stlc.md Normal file
View file

File diff suppressed because it is too large Load diff

7777
out/StlcProp.md Normal file
View file

File diff suppressed because it is too large Load diff

6
src/Logic.lagda
View file

@ -727,9 +727,9 @@ type `Bool` with two members and a type `Tri` with three members,
as defined earlier. The the type `Bool → Tri` has nine (that is,
three squared) members:
{ true → aa ; false → aa } { true → aa ; false → bb } { true → aa ; false → cc }
{ true → bb ; false → aa } { true → bb ; false → bb } { true → bb ; false → cc }
{ true → cc ; false → aa } { true → cc ; false → bb } { true → cc ; false → cc }
{true→aa;false→aa} {true→aa;false→bb} {true→aa;false→cc}
{true→bb;false→aa} {true→bb;false→bb} {true→bb;false→cc}
{true→cc;false→aa} {true→cc;false→bb} {true→cc;false→cc}
For example, the following function enumerates all possible
arguments of the type `Bool → Tri`: