The Coq mailing list

[t x <txrev319 AT gmail.com>]

Hi,

  I'm trying to learn Mtac.

  Please consider the following piece of code:

https://gist.github.com/anonymous/6ce40832829aebc2e28b

  This is what I'm happing problem with: In mtac, what is even the statement of the lemma?

  In plain Coq, (with return of option V) I can say: if I do a get after a delete, and the keys are different, I get the old value; otherwise, I get nil.

  In mtac, with return of (M V) -- what is the equivalent statement to make?

  In particular, I'm stuck on the following point: in plain Coq, the key not being in the list genrates a None. In Mtac, it generates an exception Not Found. I'm not sure how "=" is defined in this case.

Thanks!