Stream: Coq users

Topic: simple way of writing


view this post on Zulip pianke (Jun 16 2022 at 18:00):

I have function f with following arguments. f(n z:nat)(v1 v2:bool): list nat & H: count_occ (f 3 2 true false ) 1 > 2 . From H i want to extract and write z=2. What sequence of commands i should apply? unfold f or cbn[f] will work? But before that how i can extract list information from count-occ function? Any body give simple example i will be very thankful.


Last updated: Feb 08 2023 at 22:03 UTC