The Coq mailing list

[Makarius <makarius AT sketis.net>]

On Fri, 13 Apr 2012, Stéphane Glondu wrote:

> Le 12/04/2012 19:30, Xavier Leroy a écrit :
> > Short form: is there a tool / how would you go about writing a tool
> > that, given the *statement* of a Coq theorem, shows all *definitions*
> > involved in this statement, omitting all the stuff that contribute
> > only to the *proof* of the theorem?
>
> This can be done in a plugin. I've attached a proof of concept.

Stéphane seems to like the |> operator, which was intruced in Isabelle/ML 
in 1994 and later made its way into F#.  See also 
http://blogs.msdn.com/b/dsyme/archive/2011/05/17/archeological-semiotics-the-birth-of-the-pipeline-symbol-1994.aspx

Over the years, a few more variants of it were introduced that could also 
help OCaml and Coq people to express function application and composition 
concisely, without the extremism of the Haskell community in this respect.

This is the essential starter kit in OCaml notation:

  let (|>) x f = f x
  let (|->) (x, y) f = f x y

  let (@>) f g x = g (f x)
  let (@->) f g (x, y) = g (f x y)

The latter two are called #> and #-> in Isabelle/ML, but OCaml does not
allow # in symbolic identifiers as it seems.


        Makarius