Search code examples
syntaxocamlfirst-order-logic

Found ** in Ocaml, but not for exponentiation

In a book about logics (https://www.cl.cam.ac.uk/~jrh13/atp/OCaml/real.ml), I find this kind of code:

let integer_qelim =
   simplify ** evalc **
   lift_qelim linform (cnnf posineq ** evalc) cooper;;

I have seen ** before, but it was for exponentiation purposes, whereas here I do not think it is used for that, as the datatypes are not numeric. I would say it is some king of function combinator, but no idea.

I think this book was written for a version 3.06, but an updated code for 4 (https://github.com/newca12/ocaml-atp) maintains this, so ** is still used in that way that I do not understand.

Solution

  • In OCaml, you can bind to operators any behavior, e.g.,

    let ( ** ) x y = print_endline x; print_endline y

    so that "hello" ** "world" would print

    hello
world

    In the code that you reference, the (**) operator is bound to function composition:

    let ( ** ) = fun f g x -> f(g x)