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: Jun 14 2024 at 17:02 UTC