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

Multifix -> Mixfix

Browse source
This commit is contained in:
Wen Kokke 2018-07-06 15:22:47 +01:00
parent b38c1e6dcd
commit dd4ea594ef
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/plfa/Preface.lagda
View file

@ -50,7 +50,7 @@ no longer any need to learn about tactics: there is just
dependently-typed programming, plain and simple. Introduction is dependently-typed programming, plain and simple. Introduction is
always by a constructor, elimination is always by pattern always by a constructor, elimination is always by pattern
matching. Induction is no longer a mysterious separate concept, but matching. Induction is no longer a mysterious separate concept, but
corresponds to the familiar notion of recursion. Multifix syntax is corresponds to the familiar notion of recursion. Mixfix syntax is
flexible while using just one name for each concept, e.g., flexible while using just one name for each concept, e.g.,
substitution is `_[_:=_]`. The standard library is not perfect, but substitution is `_[_:=_]`. The standard library is not perfect, but
there is a fair attempt at consistency. *Propositions as types* as a there is a fair attempt at consistency. *Propositions as types* as a