4

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?

Community
  • 1
Clément
  • 5,591

2 Answers2

6

It's just two lambdas with raising and overlapping.

\documentclass{article}

\newcommand{\metalambda}{%
  \mathop{%
    \rlap{$\lambda$}%
    \mkern2mu
    \raisebox{.275ex}{$\lambda$}%
  }%
}

\begin{document}

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

\end{document}

enter image description here

The parameters might need adjusting for different fonts.

egreg
  • 1,121,712
6

Works across math styles.

\documentclass{article}
\usepackage{stackengine,trimclip,scalerel}
\def\metalambda{\mathop{\scalerel*{\stackengine{1.9pt}{$\lambda$}{%
  \kern3.4pt\smash{\clipbox{2pt -.5pt 0pt -.5pt}{$\lambda$}}}{O}{l}{F}{F}{L}}{X}\mkern1mu}}
\begin{document}
$\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
\end{document}

enter image description here

Steven B. Segletes
  • 237,551
  • 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 06 '16 at 21:38