zohaze (May 14 2023 at 11:47): zohaze (May 14 2023 at 11:47):I am using lemma In_nth from standard library. (In x l -> exists n, n < length l /\ nth n l d = x.)
I want to check the value that exist on this index is 2 then give 6 else give 0. I should pass x as argument?
zohaze (May 14 2023 at 11:50):I am using lemma In_nth from standard library. (In x l -> exists n, n < length l /\ nth n l d = x.) I want to check the value that exist on this index is 2 then give 6 else give 0. I should pass x as argument?
Last updated: Sep 15 2024 at 13:02 UTC