Stream: Program verification
Benedikt Ahrens (Sep 24 2020 at 22:02):
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?
Bryan Gin-ge Chen (Sep 24 2020 at 22:04):
open Val before the
def Eeval. Or alternatively, write
Val.Vb instead of
Bryan Gin-ge Chen (Sep 24 2020 at 22:06):
Ah, to fix
Eb as well you can use
open Exp Val.
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