Overloading `doElem`

Stream: lean4

[Vladimir Gladstein]

Hi! I am trying to overload some existing do-notation elements with a new meaning. As a minimal example, I want to allow if-condition to be a monadic computation to write code like

if pure true then return () else return ()

I was trying to active it many different ways. First I tried to expand new-if into vanilla ite:

macro_rules
  | `(doElem| if $t:term then $thn:doSeq else $els:doSeq) =>
    `(doElem| do
      let x <- $t:term
      ite x (do $thn) (do $els))

-- Works!
#check do
  if pure true then
    return ()
  else return ()
-- Doen't work
#check do
  let mut y := 0
  if pure true then
    y := 1 -- cannot modify `y`, as it is a new `do` notation
  else return ()

With this approach, I have to create a new do-notation scope for each branch, so I cannot reference to mutable variables inside those branches.
To avoid creating new branches, I decided to expand my new-if into existing one:

macro_rules
  | `(doElem| if $t:term then $thn:doSeq else $els:doSeq) =>
    `(doElem| do
      if <- $t then $thn else $els)

#check do if pure true then return () else return ()

But here the macro-expansion goes into an infinite loop
Could someone please point me to a right way of implementing such things?

[Kim Morrison]

Depending on what you're going for from "right way", there may not be one. The do syntax is not intended for user extension.