I'd prefer to keep things simple. I do like your recent syntactic innovations, but such things need to be introduced with care. And the inner syntax is considerably more delicate. Larry
> On 2 Feb 2018, at 10:50, Makarius <makar...@sketis.net> wrote: > > The general concept behind it is implicit abstraction, here with > explicit (( ... )) to delimit its scope (different notation would be > required in reality): > > ((a + _)) ~> %x. a + x > ((_ + a)) ~> %x. x + a > ((a + _ + b + _)) ~> %x y. a + x + b + y > ((_ < a)) ~> %x. x < a > > E.g. > > filter ((_ < a)) list > map ((_ - a)) list > All ((_ < a)) > Collect ((_ < a)) > > We already have implicit underscore treatment for clausal definitions, > so the above would not be totally alien. (But I am not proposing to do > anything concrete now.) _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
