Warning: this is an htmlized version!
The original is here, and
the conversion rules are here. 
-- This file:
--   http://anggtwu.net/LEAN/macro1.lean.html
--   http://anggtwu.net/LEAN/macro1.lean
--          (find-angg "LEAN/macro1.lean")
-- Author: Eduardo Ochs <eduardoochs@gmail.com>
--
-- (defun e () (interactive) (find-angg "LEAN/macro1.lean"))
-- (find-leanmetadoc "md/main/06_macros")
-- (find-leanmetadoc "md/main/01_intro#introducing-notation-defining-new-syntax")

import Lean

macro x:ident ":" t:term " ↦ " y:term : term => do `(fun $x : $t => $y)
#eval (x       :  Nat      ↦   x + 2) 2 -- 4

macro x:ident            " ↦ " y:term : term => do `(fun $x  => $y)
#eval (x                   ↦   x + 2) 2 -- 4