Outdated example in Programming in Lean

Stream: general

[Miko de Amsterdamo]

The example didn't work with my lean 3.3.0. It seems that for has become map

meta def destruct_conjunctions : tactic unit :=
repeat (do
  l ← local_context,
  first $ l.map (λ h, do
    ht ← infer_type h >>= whnf,
    match ht with
    | `(and %%a %%b) := do
      n ← mk_fresh_name,
      mk_mapp ``and.left [none, none, some h] >>= assertv n a,
      n ← mk_fresh_name,
      mk_mapp ``and.right [none, none, some h] >>= assertv n b,
      clear h
    | _ := failed
    end))