Zulip Chat Archive

Stream: new members

Topic: Constructing an ite expression without %%


view this post on Zulip Ken Roe (Jul 24 2018 at 01:10):

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?

view this post on Zulip Sebastian Ullrich (Jul 24 2018 at 23:20):

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


Last updated: May 15 2021 at 23:13 UTC