Stream: Coq users

Topic: Update values

view this post on Zulip sara lee (Oct 26 2021 at 00:25):

Function f input arguments are( a b:nat)(l:list nat). Initial values of a & b=0. f use these initial values then assign new value to b.
When write lemma that use variable b. It gives error message "Unable to find an instance for the variable b".Although I have written b=0->
b= f(0 0 l).How correct it?

view this post on Zulip Paolo Giarrusso (Oct 26 2021 at 00:55):

Any chance you need eapply instead of apply to avoid the error?

Last updated: Jun 14 2024 at 18:01 UTC