*To*: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*Subject*: [isabelle] syntax for lifted / point-free operations*From*: Peter Gammie <peteg42 at gmail.com>*Date*: Tue, 17 Nov 2015 19:29:41 +0700

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

**Attachment:
PointFree.thy**

-- http://peteg.org/

**Follow-Ups**:**Re: [isabelle] syntax for lifted / point-free operations***From:*Makarius

- Previous by Date: [isabelle] [Fwd: Re: Failing afp-2015 build]
- Next by Date: Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes
- Previous by Thread: [isabelle] [Fwd: Re: Failing afp-2015 build]
- Next by Thread: Re: [isabelle] syntax for lifted / point-free operations
- Cl-isabelle-users November 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list