Stream: Coq users

Topic: ✔ Reason about head of empty list

view this post on Zulip Pierre Castéran (Jun 06 2022 at 18:10):

You may execute exfalso; discriminate.

view this post on Zulip Roland Coeurjoly (Jun 06 2022 at 18:13):

Pierre Castéran said:

You may execute exfalso; discriminate.

Thanks! that worked!

view this post on Zulip Notification Bot (Jun 06 2022 at 18:13):

Roland Coeurjoly has marked this topic as resolved.

Last updated: Feb 08 2023 at 23:03 UTC