Email Gateway (Aug 22 2022 at 11:56): Email Gateway (Aug 22 2022 at 11:56):From: Peter Gammie <peteg42@gmail.com>
Hi,
Is anyone interested in a common syntax for point-free operations? By this I mean, for example:
abbreviation (input)
pred_conj :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" (infixr "\<^bold>\<and>" 35) where
"a \<^bold>\<and> b \<equiv> \<lambda>s. a s \<and> b s"
i.e., working in the reader monad.
Makarius suggested using \<^bold>. See the attached for the operations I’ve used thus far.
I’m not so ambitious as to attempt to make list and set comprehensions work, etc.
If there is such interest, and this is a reasonable starting point, can someone add this file to HOL/Library? There are similar operations already defined in Linear_Temporal_Logic_on_Streams, btw.
One limitation is that \<^bold> does not work so well for multi-character tokens, such as:
abbreviation (input)
pred_If :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" ("(\<^bold>if (_)/ \<^bold>then (_)/ \<^bold>else (_))" [0, 0, 10] 10) where
“\<^bold>if P \<^bold>then x \<^bold>else y \<equiv> \<lambda>s. if P s then x s else y s”
thanks,
peter
PointFree.thy
Email Gateway (Aug 22 2022 at 11:59):From: Makarius <makarius@sketis.net>
\<^bold> is a control symbol, it operates on the subsequent symbol.
Tokens are not involved here.
Multi-symbol control symbols are managed by Isabelle/jEdit: selecting a
block and applying certain actions adds or removes control symbols for
each symbol in the text.
Quotation from the "jedit" manual:
\paragraph{Control symbols.} There are some special control symbols
to modify the display style of a single symbol (without
nesting). Control symbols may be applied to a region of selected
text, either using the \emph{Symbols} panel or keyboard shortcuts or
jEdit actions. These editor operations produce a separate control
symbol for each symbol in the text, in order to make the whole text
appear in a certain style.
The manual tells more about these actions and default keyboard shortcuts.
Makarius
Last updated: Apr 27 2024 at 01:05 UTC