Constructing an ite expression without %%

Stream: new members

[Ken Roe]

I entered the following code to construct an ite expression in a meta def:

def xeval (a : ℕ) (b : ℕ) := if a=0 then 0 else b.

def beq_nat : ℕ → ℕ → bool
| 0 0 := tt
| (x+1) (y+1) := (beq_nat x y)
| (x+1) 0 := ff
| 0 (x+1) := ff


meta def evaluate_xeval_helper : expr → expr
| `(xeval %%x %%y) :=
      (app (app (app `(ite)
                     (app (app `(beq_nat))) x `(0))
                     `(0))
                     y)
| x := x

The word "ite" gets the error

failed to synthesize type class instance for
evaluate_xeval_helper : expr → expr,
_x : list level,
x y : expr
⊢ reflected ite

How do I fix this error?

[Sebastian Ullrich]

The error is because the universe parameter of ite could not be inferred. If you use the full quotation

`(if beq_nat %%x 0 then (0 : nat) else %%y)

it should work