\definetyping[lambda][option=LAM,style=sans]
\definetype[lam][option=LAM,style=sans]
+\installprettytype [TRANS] [TRANS]
+\definetyping[trans][option=TRANS,style=normal,before=,after=]
+
% An (invisible) frame to hold a lambda expression
\define[1]\lamframe{
% Put a frame around lambda expressions, so they can have multiple
β-reduction and function inlining below, all function-typed expressions should
be lambda abstractions or global identifiers.
-\transform{η-abstraction}
-{
-\lam{E :: * -> *}
-
-\lam{E} is not the first argument of an application.
-
-\lam{E} is not a lambda abstraction.
-
-\lam{x} is a variable that does not occur free in E.
-
-\conclusion
-
-\trans{E}{λx.E x}
-}
+\starttrans
+E \lam{E :: * -> *}
+-------------- \lam{E} is not the first argument of an application.
+λx.E x \lam{E} is not a lambda abstraction.
+ \lam{x} is a variable that does not occur free in \lam{E}.
+\stoptrans
\startbuffer[from]
foo = λa -> case a of
hardware translation is available, because its actual definition is not
translatable. A user-defined function is any other function.
+\starttrans
+x = E
+~
+x Y0 ... Yi ... Yn \lam{Y_i} is not of a runtime representable type
+--------------------------------------------- \lam{Y_i} is not a local variable reference
+x' = λy0 ... yi-1 f0 ... fm yi+1 ... yn . \lam{f0 ... fm} = free local vars of \lam{Y_i}
+ E y0 ... yi-1 Yi yi+1 ... yn
+~
+x' y0 ... yi-1 f0 ... fm Yi+1 ... Yn
+\stoptrans
+
\transform{Argument propagation}
{
\lam{x} is a global variable, bound to a user-defined function
## Context PDF build
pdfOutput = env.Context(LATEX_PROJECT)
Depends(pdfOutput, 'pret-lam.lua')
+Depends(pdfOutput, 'pret-trans.lua')
env.Alias('pdf', LATEX_PROJECT + '.pdf')
# Keep below code happy