pianke (Jun 16 2022 at 18:00): 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: Oct 01 2023 at 17:01 UTC