Stream: Coq users

Topic: Update values

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?

Paolo Giarrusso (Oct 26 2021 at 00:55):

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

Last updated: Oct 03 2023 at 20:01 UTC