Open Vtec234 opened 1 year ago
I think the return
is operating at the wrong scope:
def foo₁ (T : Q(Type)) : MetaM Bool := do
if let ~q(Prop) := T then
return ()
return true
It's returning from the inner macro, not the outer do block
Here's a slightly more damning example:
import Qq
open Qq Lean
def foo₂ (T : Q(Type)) : MetaM Bool := do
let x : Unit ← match T with
| ~q(Prop) => return true
| _ => return true
return false
#eval foo₂ q(Nat) -- false
#eval foo₂ q(Int) -- false
I added a lot of test-cases in #27
A possible solution is discussed at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Converting.20from.20doSeq.20to.20doSeqItem/near/402223969
Consider the snippet below. I would expect the two functions
foo₁
andfoo₂
to be equivalent and both to work, howeverfoo₁
fails to elaborate with a type error.