Problem with pattern matching in function definition

Stream: Program verification

[Benedikt Ahrens]

Hi,
In the following (non-sensical) example code

inductive Exp : Type
| Ei : ℕ → Exp
| Eb : bool → Exp

inductive Val : Type
| Vi : ℕ → Val
| Vb : bool → Val

def Eeval : Exp → Val
| (Ei n) := Vi n
| (Eb b) := Vb b

I am getting the following errors:

 22:4 error
equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
 23:3 error
invalid application, function expected
 23:12 error
unknown identifier 'Vi'
 24:3 error
invalid application, function expected
 24:12 error
unknown identifier 'Vb'

(where line 22 is the one containing def Eeval : Exp → Val.
Could you tell me what I am doing wrong?
Benedikt

[Bryan Gin-ge Chen]

Try adding open Val before the def Eeval. Or alternatively, write Val.Vi and Val.Vb instead of Vi and Vb.

[Bryan Gin-ge Chen]

Ah, to fix Ei and Eb as well you can use open Exp Val.

[Benedikt Ahrens]

Thanks, that fixes it! (I realize I should have posted this in the stream "new members" instead...)