unbind macro for do notation

Stream: general

[Frederick Pu]

I'm trying to make a do sugar that allows you to force a doElem to be left associated. However, I get the following error

import Lean
import Qq

open Lean Qq
open Lean Parser Meta Elab Term Command

syntax "unbind " term: doElem

macro_rules
  | `(term| do $seq₁:doElem (do unbind $t:term; $el:doElem)) =>
    `(term| do (do $seq₁:doElem $t:term) $el:doElem)

def dd : Id Nat := do
  let y := 5; (do unbind 10; pure 10)

/- unexpected do-element of kind doElemUnbind_:
unbind 10
-/

[Robin Arnez]

You're probably looking for doSeqItem* and not doElem

[Frederick Pu]

thx! is there anyway to get rid of the do notation before the unbind?

import Lean
import Qq

open Lean Qq
open Lean Parser Meta Elab Term Command

syntax "unbind " term : doElem

macro_rules
  | `(term| do $seq₁:doSeqItem* ((unbind $t:term : doSeqItem) $seq₂:doSeqItem*)) =>
    `(term| do (do $seq₁:doSeqItem* $t:term) $seq₂:doSeqItem*)

def dd : Id Nat := do
  let x := 2;
  let mut y := 5;
  (unbind pure ()
  for i in List.range 20 do
    y := y + 1 + i
  )
  for j in List.range 40 do
    y := y + x + j
  return y

[Frederick Pu]

im currently getting unexpected token 'unbind'; expected ')', '_', identifier or level