`If` inside `conv`

[jeremysalwen]

Prerequisites

• [ x] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

if doesn't work inside of conv mode.

Steps to Reproduce

import Lean

open Lean

opaque foo : Int → Int
axiom foo.pos (x : Int) (h : x ≥ 0) : foo x =  1
axiom foo.neg (x : Int) (h : ¬(x ≥ 0)) : foo x = -1

example : foo = λ (x : Int) => if x ≥ 0 then 1 else -1 :=
by

  conv =>
    lhs; enter [x]

    if h : x ≥ 0 then
      rw [foo.pos x h]
    else
      rw [foo.neg x h]

  done

Expected behavior: This proof to work

Actual behavior: if tactic is not accepted, giving "expected command" error.

Reproduces how often: 100%

Versions

Lean (version 4.0.0-nightly-2023-01-21, commit a125a36, Release)
Windows 10.

Additional Information

On the Zulip Chat, Tomas Skrivan posted a working implementation for if and match inside of conv, including the example proof above:
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/If.20and.20match.20in.20conv.20mode