Zulip Chat Archive

Stream: Program verification

Topic: Problem with pattern matching in function definition


view this post on Zulip Benedikt Ahrens (Sep 24 2020 at 22:02):

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

view this post on Zulip Bryan Gin-ge Chen (Sep 24 2020 at 22:04):

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

view this post on Zulip Bryan Gin-ge Chen (Sep 24 2020 at 22:06):

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

view this post on Zulip Benedikt Ahrens (Sep 24 2020 at 22:14):

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


Last updated: May 08 2021 at 22:13 UTC