Bart Jacobs, in his book Categorical Logic and Type Theory, uses a very cool notation for "meta-lambda abstraction":

lambda double bar

In context, it looks like this: lambda lambda, two lambda superposed

It sorts of remind of the haskell logo, but it looks like this symbol does not exists (I checked the usual resources, listed here).

Did anyone ever meet this symbol? Any suggestion on how to typeset it?

2 Answers 2


It's just two lambdas with raising and overlapping.




$\metalambda x\mathpunct{.}f(x)$


enter image description here

The parameters might need adjusting for different fonts.


Works across math styles.

  \kern3.4pt\smash{\clipbox{2pt -.5pt 0pt -.5pt}{$\lambda$}}}{O}{l}{F}{F}{L}}{X}\mkern1mu}}
$\lambda x:\sigma.M\quad \metalambda x.f(x)$\par
$\scriptstyle\lambda x:\sigma.M\quad \metalambda x.f(x)$\par
$\scriptscriptstyle\lambda x:\sigma.M\quad \metalambda x.f(x)$\par

enter image description here

  • 1
    Thanks for your convincing and portable answer, but egreg's answer's simplicity in terms of package make his answer more easy to use.
    – Clément
    Nov 6, 2016 at 21:38

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .