From dd4ea594ef7c6e16ca4c1bd14c7002cbf1ec4473 Mon Sep 17 00:00:00 2001 From: Wen Kokke Date: Fri, 6 Jul 2018 15:22:47 +0100 Subject: [PATCH] Multifix -> Mixfix --- src/plfa/Preface.lagda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/plfa/Preface.lagda b/src/plfa/Preface.lagda index 15be36c7..af831ec9 100644 --- a/src/plfa/Preface.lagda +++ b/src/plfa/Preface.lagda @@ -50,7 +50,7 @@ no longer any need to learn about tactics: there is just dependently-typed programming, plain and simple. Introduction is always by a constructor, elimination is always by pattern 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., substitution is `_[_:=_]`. The standard library is not perfect, but there is a fair attempt at consistency. *Propositions as types* as a