Stream: Coq users

Topic: avoid empty list


view this post on Zulip pianke (Apr 06 2023 at 02:56):

H1: (m::m1::t)<> [] ->
f'(a c (m::m1::t))=a::a0::t'
Goal statement:
match
  f'(a c (m::m1::t))
    with
| [] => false
|h::t=> .....

Which command i should apply to avoid empty list case?

view this post on Zulip Pierre Castéran (Apr 06 2023 at 05:48):

Did you try rewrite H1 ?

view this post on Zulip pianke (Apr 08 2023 at 11:24):

It works.Thank you.


Last updated: Oct 13 2024 at 01:02 UTC