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

fix to Preface

Browse source
This commit is contained in:
wadler 2018-07-06 10:12:31 -03:00
parent d9b0872a66
commit 4a558614bf
1 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/plfa/Preface.lagda
View file

@ -12,11 +12,11 @@ either the proof of the proposition or as a programme of the
corresponding type. Further still, simplification of proofs
corresponds to evaluation of programs.
The title of this book also has two readings. It may be parsed as
"(Programming Language Foundations) in Agda" or "Programming (Language
Foundations) in Agda" — the specifications we will write in the proof
assistant Agda both describe programming languages and are themselves
programmes.
Accordingly, the title of this book also has two readings. It may be
parsed as "(Programming Language) Foundations in Agda" or "Programming
(Language Foundations) in Agda" — the specifications we will write in
the proof assistant Agda both describe programming languages and are
themselves programmes.
## Personal remarks